How is the morphism of composition in the enriched category of modules constructed? I asked this a week ago at MSE, but without success.
I am studying enriched categories and I have a feeling that I am doing something wrong because all the way each step, each elementary proposition, requires enormous efforts and a lot of time from me. In particular, I am now stuck in the question of how the structure of the enriched category is introduced into the category $_AV$ of modules over a given monoid $A$ in a (symmetric) closed monoidal category $V$.
I asked this earlier (in April) at MSE:

if we consider an arbitrary closed monoidal category $V$ and take an arbitrary monoid $A$ in $V$, will the category $_A V$ of all left $A$-modules be an enriched category over $V$?

People explained to me the construction of the object of morphisms $V(M,N)$, I am grateful to them, and I accepted their answer, but not long ago I decided to write down the proof and (forgive me for my carelessness) I realized that I do not understand how the "enriched" composition morphism is constructed in $_AV$:
$$
\circ_{L,M,N}:V(M,N)\otimes V(L,M)\to V(L,N).
$$
I think that this must be the "lift to the equalizer" of the cone
\begin{equation}\tag{1}
V(M,N)\otimes V(L,M)\to \underline{\operatorname{Hom}}(M,N)\otimes \underline{\operatorname{Hom}}(L,M)\to \underline{\operatorname{Hom}}(L,N)
\end{equation}
for the pair of morphisms that define $V(L,N)$ as their equalizer:
$$
\underline{\operatorname{Hom}}(L,N)\to \underline{\operatorname{Hom}}(A\otimes L,N)
$$
and
$$
\underline{\operatorname{Hom}}(L,N)\to \underline{\operatorname{Hom}}(L, \underline{\operatorname{Hom}}(A,N)) \to \underline{\operatorname{Hom}}(A\otimes L,N)
$$
(here $\underline{\operatorname{Hom}}$ means the inner hom-functor in $V$).
But the problem for me is that I don't understand why (1) is indeed a cone for this pair, i.e.

why the two morphisms
$$
V(M,N)\otimes V(L,M)\to \underline{\operatorname{Hom}}(M,N)\otimes \underline{\operatorname{Hom}}(L,M)\to \underline{\operatorname{Hom}}(L,N)\to \underline{\operatorname{Hom}}(A\otimes L,N)
$$
and
$$
V(M,N)\otimes V(L,M)\to \underline{\operatorname{Hom}}(M,N)\otimes \underline{\operatorname{Hom}}(L,M)\to \underline{\operatorname{Hom}}(L,N)\to \underline{\operatorname{Hom}}(L, \underline{\operatorname{Hom}}(A,N)) \to \underline{\operatorname{Hom}}(A\otimes L,N)
$$
coincide.

My proof requires 40 diagrams, but this is only a draft, because I deduce everything from the following lemma, which still is a puzzle for me:

Lemma. For each objects $A$, $X$, $Y$ and each morphism $\mu:A\otimes Y\to Y$ the following two morphisms coincide:
$$
\underline{\operatorname{Hom}}(X,Y)\otimes A\otimes X\to 
\underline{\operatorname{Hom}}(X,\underline{\operatorname{Hom}}(A,Y))\otimes A\otimes X\to 
\underline{\operatorname{Hom}}(A\otimes X,Y)\otimes A\otimes X\to Y
$$
(were the first arrow is generated by the arrow $Y\to\underline{\operatorname{Hom}}(A,Y)$, which corresponds to the morphism $\mu:A\otimes Y\to Y$), and
$$
\underline{\operatorname{Hom}}(X,Y)\otimes A\otimes X\to 
A\otimes \underline{\operatorname{Hom}}(X,Y)\otimes X\to 
A\otimes Y\to Y
$$
(were the last arrow is the morphism $\mu:A\otimes Y\to Y$).

This looks very strange to me (because it's difficult for me to believe that everything can be so complicated), but I don't see how this can be simplified, nor how to prove this lemma. Can anybody help me?
In Russia where I live, such problems are traditionally resolved by communication with experts, but as far as I know, there are no experts in category theory left in Russia.
 A: 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}$$
A: $\def\mod{\text{Mod}}$Let's call $[X,Y]$ the internal hom of $X$ and $Y$, and $\mod_A(X,Y)$ the sub-$V$-object of $A$-module homomorphisms defined as the equaliser here.
Let $f : \mod_A(M,N)$ and $g : \mod_A(L,M)$, so that
$$
f \cdot \rho_M = \rho_N\cdot(A\otimes f)
\tag{If}$$
and
$$
g \cdot \rho_L = \rho_M \cdot(A\otimes g)
\tag{Ig}$$
Fact. The juxtaposition of two squares in a diagram

when precomposed with the map $\mod_A(M,N)\otimes \mod_A(L,M) \hookrightarrow [M,N]\otimes [L,M]$ at the top left corner, commutes.
Of course I have to tell you how the solid maps are defined:

*

*the leftmost and central solid vertical map is composition $c_{LMN}$ in the category $\mathscr{V}$; there is a universal way to obtain $c_{LMN}$ as mates of the maps that witness how hom functors are $\mathscr{V}$-functors

*the horizontal upper and lower pairs of maps are the pair of morphisms you equalise to obtain $\mod_A(M,N)$, $\mod_A(L,N)$, etc.

*careful: the lower row is an equaliser, but the upper one is not. It is, however, a cone.

*the rightmost vertical map arises from the map $M\cong I\otimes M \overset{e\otimes M}\to A\otimes M$, where $e$ is the unit of the monoid $A$ for which $M$ is a module.

A bit sloppily, this means that if we choose $(f,g)\in [M,N]\otimes [L,M]$ such that $f :  \mod_A(M,N)$ and $g : \mod_A(L,M)$, then chasing their image along the possible compositions in the above diagram yields the same result.
This is what you should prove in order to obtain that there is a unique dotted map
$$ \hat c_{LMN} : \mod_A(M,N)\otimes \mod_A(L,M) \to \mod_A(L,N) $$
making the left-most square commutative, and thus restricting the composition $c_{LMN} : [M,N]\otimes [L,M] \to [L, N]$.
It doesn't seem problematic to me to prove this statement; you just need the usual diagram chasing, plus (If) and (Ig) above.
A bit more effort is required if you want to show explicitly that the $\hat c_{LMN}$ "are compositions", in the sense that they are associative and unital. However, (again a bit sloppily) "they arise as restrictions of a composition rule".
