$\newcommand{\rotimes}{\hat\otimes}$
Here's a sketch of a proof, I suspect it should be enough :
Step 1 : Prove the result in an un-enriched case, that is : if $(\mathcal V, \otimes, I)$ is a monoidal category, $R$ a monoid-object in $\mathcal V$, then $X\mapsto X\otimes R$ is left-adjoint to the forgetful functor $(R-mod)^0 \to \mathcal V$ (where $(R-mod)^0$ is the unenriched category of $R$-modules). This involves some reasonable diagram-chasing, if you want more details I can add them but it's not too hard : define the obvious adjunction maps and draw the correct diagrams to see that they are inverse.
Step 2: Use the Yoneda lemma. More precisely, let $(\mathcal V,\otimes, I)$ be a closed symmetric bicomplete monoidal category, $(\mathcal M, \rotimes, e)$ a $\mathcal V$-enriched monoidal category ($\rotimes$ is an enriched bifunctor - though to be fair I'm not sure it needs to be enriched) which is tensored over $\mathcal V$, with tensor $\odot$.
I'll use the following notations : $\hom$ is the hom-set in $\mathcal V$ and in $\mathcal M$, $\newcommand{\rhom}{\mathcal{Hom}}$ $\rhom$ is the hom-$\mathcal{V}$-object in $\mathcal M$ (note that we have, by definition of hom-set for an enriched category : $\hom(X,Y) = \hom(I, \rhom(M,N))$ for $M,N\in \mathcal M$). Then the tensoring $\odot$ should satisfy $\hom(Y, \rhom(M,N)) \cong \hom(Y\odot M,N)$ (you can probably even ask for an enriched adjunction here, but it's not necessary, so I'm not getting into that)
Tensoring should also be compatible with $\rotimes$ in the sense that $Y\odot (M\rotimes N) \cong (Y\odot M)\rotimes N$ and this isomorphism should be compatible with all the data in $\mathcal M$: associator, unitor.
With all this under the belt we can see :
For any monoid-object $R$ in $\mathcal M$ and any $R$-module $M$, $Y\odot M$ is canonically an $R$-module with the obvious structure maps. Then we have the following string of isomorphisms $$\hom(Y, \rhom(X,M)) \cong \hom(Y\odot X, M) \cong \hom_{(R-mod)^0}(Y\odot X\rotimes R, M) \cong \hom(Y, R-mod_{\mathcal M}(X\rotimes R, M))$$
where $R-mod_{\mathcal M}$ is the enriched category of $R$-modules as you have defined it (the definition makes sense for any $\mathcal M$ with the properties I gave), and where the isomorphisms are justified as follows :
the first one is just the $\odot \dashv \rhom$ adjunction; the second one is from step 1 (since we're dealing with honest modules), and the third one is to justify :
Note that a morphism $Y\to R-mod_{\mathcal M}(M,N)$ ($M,N$ arbitrary $R$-modules) is the same as a morphism $Y\to \rhom(M,N)$ equalizing the two arrows $\rhom(M,N)\rightrightarrows \rhom(M\rotimes R, N)$. By $\odot \dashv \rhom$ adjunction, this is the same as a map $Y\odot M \to N$ making the following diagram commute :
$\require{AMScd} \begin{CD}Y\odot M @>>> N \\
@AAA @AAA \\
Y\odot M \rotimes R @>>> N\rotimes R\end{CD}$
which is precisely a module morphism $Y\odot M\to N$; and then we apply this to $X\rotimes R$ and $M$ instead of $M,N$.
It follows (from the unenriched Yoneda lemma) that we have the desired enriched adjunction.
We then check that $\mathcal{V^C}$ satisfies the correct hypothesis, I did that bit in my head so I'm not 100% sure but it should work.
Nice work so far! I think breaking down the definition of this functor into smaller pieces will be helpful.
Given a morphism $g : b' \to b$ and an object $c$, we define $[g,1_c] : [b,c] \to [b',c]$ to be
$$\eta_{[b,c],b',c}(\eta_{[b,c],b,c}^{-1}(1_{[b,c]}) \circ (1_{[b,c]} \otimes g)).$$
Then we verify two conditions:
- $[g_1 \circ g_2, 1_c] = [g_2, 1_c] \circ [g_1, 1_c]$ for all morphisms $g_1 : b' \to b$, $g_2 : b'' \to b'$, and all objects $c$.
- $[1_{b'}, h] \circ [g,1_c] = [g, 1_{c'}] \circ [1_b, h]$ for all morphisms $g : b' \to b$ and $h : c \to c'$.
From these two facts it follows that defining $[g, h] = [g, 1_{c'}] \circ [1_b, h]$ makes $[{-},{=}]$ into a functor. This is general phenomenon: to define a functor $C_1 \times C_2 \to D$, you just need to describe the functoriality in each component and then check that they "commute" (in the sense of condition 2 above).
Unfortunately I don't have time to write a full answer right now, but I hope this helps you finish the proof -- the benefit of doing it this way is that you only have to deal with two morphisms (instead of four) at any time.
For condition 1, we equivalently need to verify that the following diagram commutes:
(Check that this is really equivalent!). The three morphisms in this diagram also appeared in the commutative squares witnessing the naturality of $\eta$ (the square you drew in your post). So we paste those squares around the outside as follows:
Now check that the squares & triangles marked in red commute, and use the fact that the colored arrows are isomorphisms to deduce that the inner triangle commutes.
Apologies for the poor handwriting, I hope it's still understandable!
Best Answer
Let $\epsilon^{A}_B$ be the map $\eta_{\frac{B}{A},A,B}^{-1}(1_{\frac{B}{A}}) $, or in other words, let $\epsilon^{A}$ be the counit of the adjunction $? \otimes_A\dashv \frac{??}{A}$, and similarly for $B,C$. Then the inverse of $\eta_{A,B,C}$ is the map $g\mapsto \epsilon^{B}_C \circ (g\otimes B)$. Moreover, the inner composition $$\frac{C}{B}\otimes\frac{B}{A}\to\frac{C}{A}$$ is the image of the composite $$\frac{C}{B}\otimes\frac{B}{A}\otimes A\stackrel{\frac{C}{B}\otimes \epsilon_{B}^{A}}{\longrightarrow} \frac{C}{B}\otimes B \stackrel{ \epsilon_{C}^B}{\longrightarrow} C$$ under the bijection $\eta_{\frac{C}{B}\otimes\frac{B}{A},A,C}$.
As a consequence, and because of the naturality of $\eta$, we find that \begin{align}\bullet_{A,B,C}\circ (\widehat{\psi}\otimes\widehat{\varphi}) & = \eta_{\frac{C}{B}\otimes\frac{B}{A},A,C}\left(\epsilon^B_C\circ \left(\frac{C}{B}\otimes\epsilon^{A}_B\right) \right) \circ (\widehat{\psi}\otimes \widehat{\varphi})\\ & = \eta_{I\otimes I,A,C}\left(\epsilon^B_C\circ \left(\frac{C}{B}\otimes\epsilon^{A}_B\right) \circ (\widehat{\psi}\otimes \widehat{\varphi}\otimes A)\right) \\ & = \eta_{I\otimes I,A,C}\left(\epsilon^B_C\circ \left(\widehat{\psi}\otimes (\epsilon^{A}_B \circ ( \widehat{\varphi}\otimes A))\right) \right) \\ & = \eta_{I\otimes I,A,C}\left(\epsilon^B_C \circ \left(\widehat{\psi}\otimes (\varphi\circ \lambda_A) \right) \right) \\ & = \eta_{I,A,C}\left(\epsilon^B_C \circ (\widehat{\psi}\otimes B) \circ (I\otimes (\varphi\circ \lambda_A)) \right) \\ & = \eta_{I\otimes I,A,C}\left(\psi\circ \lambda_B \circ (I\otimes (\varphi\circ \lambda_A)) \right)\\ & = \eta_{I\otimes I,A,C}\left(\psi\circ \varphi\circ \lambda_A \circ \lambda_{I\otimes A} \right) \\ & = \eta_{I\otimes I,A,C}\left((\psi\circ \varphi)\circ \lambda_A \circ (\lambda_{I}\otimes A) \right)\\ & = \eta_{I,A,C}\left((\psi\circ \varphi)\circ \lambda_A \right)\circ \lambda_{I} \\ & = \widehat{\psi\circ \varphi} \circ \lambda_I\end{align} (with some associators missing, but it should work).