I’ll change notation slightly, writing $\newcommand{\V}{\mathcal{V}}\V(A,B)$ and $\newcommand{\AV}{{}_{A}\! \V}\AV(M,N)$ respectively for the $\V$-hom-objects and $A$-module-homomorphism objects respectively.

The first thing I’d do is just write down the ordinary algebraic proof that a composition of module homomorphisms is a module homomorphism: $$ (gf)(am) = g(f(am)) = g(a(fm)) = a(g(fm)) = a((gf)m).$$

This is very simple — just four steps! This makes me pretty confident that the categorical proof shouldn’t be too bad. Generally, a simple algebraic proof should become a reasonably simple categorical proof.

So trying for the categorical proof: as you say, it comes down to showing that the map $$\newcommand{\x}{\otimes}\AV(M,N) \x \AV(N,P) \to \V(M,N) \x \V(N,P) \to \V(M,P)$$ equalises the two maps $\V(M,P) \to \V(A \x M, P)$ that define $\AV(M,P)$. This means showing an equality of two maps $\AV(M,N) \x \AV(N,P) \to \V(A \x M,P)$; so it corresponds by transpose to an equality of maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$.

Now it’s ready for diagram-chasing: I wrote down the desired LHS as a vertical composite and worked rightwards from it until I could find the RHS. Based on the algebraic proof above, I expected 4 main steps, in order: the definition of composition; the $(M,N)$ homomorphism condition; the $(N,P)$ homomorphism condition; and then the definition of composition again. So I wrote those each down on the side to know what to look for. Using those, together with the “interchange” rule $(\alpha \x B)(A' \x \beta) = (A \x \beta)(\alpha \x B')$, the following diagram pretty much wrote itself:

(although the layout was of course terrible the first time; this version is rewritten for readability). Here the vertical composites down the left- and right-hand sides are exactly the maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$ we needed to show were equal. Overall, as hoped, it really isn’t too bad in the end — one big diagram, built of 9 commutative squares/hexagons.

I’ll change notation slightly, writing $\newcommand{\V}{\mathcal{V}}\V(A,B)$ and $\newcommand{\AV}{{}_{A}\! \V}\AV(M,N)$ respectively for the $\V$-hom-objects and $A$-module-homomorphism objects respectively.

The first thing I’d do is just write down the ordinary algebraic proof that a composition of module homomorphisms is a module homomorphism: $$ (gf)(am) = g(f(am)) = g(a(fm)) = a(g(fm)) = a((gf)m).$$

This is very simple — just four steps! This makes me pretty confident that the categorical proof shouldn’t be too bad. Generally, a simple algebraic proof should become a reasonably simple categorical proof.

So trying for the categorical proof: as you say, it comes down to showing that the map $$\newcommand{\x}{\otimes}\AV(M,N) \x \AV(N,P) \to \V(M,N) \x \V(N,P) \to \V(M,P)$$ equalises the two maps $\V(M,P) \to \V(A \x M, P)$ that define $\AV(M,P)$. This means showing an equality of two maps $\AV(M,N) \x \AV(N,P) \to \V(A \x M,P)$; so it corresponds by transpose to an equality of maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$.

Now it’s ready for diagram-chasing: I wrote down the desired LHS as a vertical composite and worked rightwards from it until I could find the RHS. Based on the algebraic proof above, I expected 4 main steps, in order: the definition of composition; the $(M,N)$ homomorphism condition; the $(N,P)$ homomorphism condition; and then the definition of composition again. So I wrote those each down on the side to know what to look for. Using those, together with the “interchange” rule $(\alpha \x B)(A' \x \beta) = (A \x \beta)(\alpha \x B')$, the following diagram pretty much wrote itself:

(although the layout was of course terrible the first time; this version is rewritten for readability). Here the vertical composites down the left- and right-hand sides are exactly the maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$ we needed to show were equal. Overall, as hoped, it really isn’t too bad in the end — one big diagram, built of 9 commutative squares/hexagons.

Edit in response to comments: Here I’m taking $\AV(M,N)$ to be defined as the equaliser of the maps $f_1, f_2 : \V(M,N) \to \V(A \x M, N)$ defined as the transposes of $$\begin{align} \newcommand{\ev}{\mathrm{ev}} g_1 & := \ev_{M,N}(\alpha_M \x \V(M,N)) : A \x M \x \V(M,N)\to M \x \V(M,N) \to N \\ g_2 & := \alpha_N (A \x \ev_{M,N}) : A \x M \x \V(M,N) \to A \x N \to N. \end{align}$$

With these definitions, no extra lemmas are needed for the proof above. On the other hand, you say you’re using the definition given by Martin Brandenburg here, specifying the maps in the equaliser as

$$\begin{align} f_1' & := (\alpha_M)^* : \V(M,N) \to \V(A \x M,N) \\ f_2' & := \chi (\bar{\alpha_N})_* : \V(M,N) \to \V(M,\V(A, N)) \to \V(A \x M, N) \end{align}$$

Checking these agree with my $f_1$, $f_2$ depends slightly on which definitions you’re assuming for things like $(-)_*$ and the isomorphism $\chi : \V(M,\V(A, N)) \to \V(A \x M, N)$. Under the definitions I’m used to, $f_1 = f_1'$ is automatic — “the transpose of $\ev_{M,N}(\alpha_M \x \V(M,N))$” is what I know as the standard definition for $(\alpha_M)^*$. For $f_2 = f_2'$ — essentially the lemma you mention — it suffices to show that $f_2'$ corresponds under transpose to $g_2$. By definition (at least as I take it), $\chi$ corresponds to $\ev_{A,N}(A \x \ev_{M,\V(A,N)}) : A \x M \x \V(M,\V(A, N)) \to N$. So $f_1' = \chi (\bar{\alpha_N})_*$ corresponds to $$\begin{align} \ev_{A,N}(A \x \ev_{M,\V(A,N)})(A \x M \x (\bar{\alpha_N})_*) & = \ev_{A,N}(A \x (\ev_{M,N}(M \x (\bar{\alpha_N})_*))) \\ & = \ev_{A,N}(A \x (\bar{\alpha_N} \ev_{M,N})) \\ & = \ev_{A,N}(A \x \bar{\alpha_N})(A\x \ev_{M,N}) \\ & = \alpha_N (A \x \ev_{M,N}) \\ & = g_2.\end{align}$$

I’ll change notation slightly, writing $\newcommand{\V}{\mathcal{V}}\V(A,B)$ and $\newcommand{\AV}{{}_{A}\! \V}\AV(M,N)$ respectively for the $\V$-hom-objects and $A$-module-homomorphism objects respectively.

The first thing I’d do is just write down the ordinary algebraic proof that a composition of module homomorphisms is a module homomorphism: $$ (gf)(am) = g(f(am)) = g(a(fm)) = a(g(fm)) = a((gf)m).$$

This is very simple — just four steps! This makes me pretty confident that the categorical proof shouldn’t be too bad. Generally, a simple algebraic proof should become a reasonably simple categorical proof.

So trying for the categorical proof: as you say, it comes down to showing that the map $$\newcommand{\x}{\otimes}\AV(M,N) \x \AV(N,P) \to \V(M,N) \x \V(N,P) \to \V(M,P)$$ equalises the two maps $\V(M,P) \to \V(A \x M, P)$ that define $\AV(M,P)$. This means showing an equality of two maps $\AV(M,N) \x \AV(N,P) \to \V(A \x M,P)$; so it corresponds by transpose to an equality of maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$.

Now it’s ready for diagram-chasing: I wrote down the desired LHS as a vertical composite and worked rightwards from it until I could find the RHS. Based on the algebraic proof above, I expected 4 main steps, in order: the definition of composition; the $(M,N)$ homomorphism condition; the $(N,P)$ homomorphism condition; and then the definition of composition again. So I wrote those each down on the side to know what to look for. Using those, together with the “interchange” rule $(\alpha \x B)(A' \x \beta) = (A \x \beta)(B' \x \alpha)$, the following diagram pretty much wrote itself:

(although the layout was of course terrible the first time; this version is rewritten for readability). Here the vertical composites down the left- and right-hand sides are exactly the maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$ we needed to show were equal. Overall, as hoped, it really isn’t too bad in the end — one big diagram, built of 9 commutative squares/hexagons.

I’ll change notation slightly, writing $\newcommand{\V}{\mathcal{V}}\V(A,B)$ and $\newcommand{\AV}{{}_{A}\! \V}\AV(M,N)$ respectively for the $\V$-hom-objects and $A$-module-homomorphism objects respectively.

The first thing I’d do is just write down the ordinary algebraic proof that a composition of module homomorphisms is a module homomorphism: $$ (gf)(am) = g(f(am)) = g(a(fm)) = a(g(fm)) = a((gf)m).$$

This is very simple — just four steps! This makes me pretty confident that the categorical proof shouldn’t be too bad. Generally, a simple algebraic proof should become a reasonably simple categorical proof.

So trying for the categorical proof: as you say, it comes down to showing that the map $$\newcommand{\x}{\otimes}\AV(M,N) \x \AV(N,P) \to \V(M,N) \x \V(N,P) \to \V(M,P)$$ equalises the two maps $\V(M,P) \to \V(A \x M, P)$ that define $\AV(M,P)$. This means showing an equality of two maps $\AV(M,N) \x \AV(N,P) \to \V(A \x M,P)$; so it corresponds by transpose to an equality of maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$.

Now it’s ready for diagram-chasing: I wrote down the desired LHS as a vertical composite and worked rightwards from it until I could find the RHS. Based on the algebraic proof above, I expected 4 main steps, in order: the definition of composition; the $(M,N)$ homomorphism condition; the $(N,P)$ homomorphism condition; and then the definition of composition again. So I wrote those each down on the side to know what to look for. Using those, together with the “interchange” rule $(\alpha \x B)(A' \x \beta) = (A \x \beta)(\alpha \x B')$, the following diagram pretty much wrote itself:

(although the layout was of course terrible the first time; this version is rewritten for readability). Here the vertical composites down the left- and right-hand sides are exactly the maps $A \x M \x \AV(M,N) \x \AV(N,P) \to P$ we needed to show were equal. Overall, as hoped, it really isn’t too bad in the end — one big diagram, built of 9 commutative squares/hexagons.