[proofplan]
We establish the isomorphism by composing two previously proved results. First, we apply the associativity isomorphism (isomorphism (2) of the [S-Module Isomorphisms Under Extension of Scalars](/theorems/2917)) to rewrite $S \otimes_R (N \otimes_R N')$ as $(S \otimes_R N) \otimes_R N'$. Then we apply the [Base Change for Extension of Scalars](/theorems/2916) to rewrite $(S \otimes_R N) \otimes_R N'$ as $(S \otimes_R N) \otimes_S (S \otimes_R N')$, since $S \otimes_R N$ is an $S$-module and $N'$ is an $R$-module. The composite is the desired $S$-module isomorphism.
[/proofplan]
[step:Apply associativity to rewrite $S \otimes_R (N \otimes_R N')$ as $(S \otimes_R N) \otimes_R N'$]
By the associativity isomorphism for $\otimes_R$ (isomorphism (2) of the [S-Module Isomorphisms Under Extension of Scalars](/theorems/2917), applied with $M = S$, first $R$-module $= N$, second $R$-module $= N'$; the hypothesis that $M$ is an $S$-module is satisfied since $S$ is an $S$-module via its own multiplication), there is an $S$-module isomorphism
\begin{align*}
\alpha: S \otimes_R (N \otimes_R N') &\xrightarrow{\;\sim\;} (S \otimes_R N) \otimes_R N'
\end{align*}
sending $s \otimes (n \otimes n') \mapsto (s \otimes n) \otimes n'$ on pure tensors.
[guided]
Why does this isomorphism exist? The associativity of the tensor product states that for any ring $R$ and $R$-modules $A, B, C$, there is a canonical isomorphism $A \otimes_R (B \otimes_R C) \cong (A \otimes_R B) \otimes_R C$. Here we take $A = S$, $B = N$, $C = N'$. Since $S$ carries an $S$-module structure, the associativity isomorphism is not merely $R$-linear but $S$-linear: the $S$-action on the left-hand side is $t \cdot (s \otimes (n \otimes n')) = (ts) \otimes (n \otimes n')$, and on the right-hand side it is $t \cdot ((s \otimes n) \otimes n') = (ts \otimes n) \otimes n'$. These are mapped to each other by $\alpha$, confirming $S$-linearity.
[/guided]
[/step]
[step:Apply the base change isomorphism to rewrite $(S \otimes_R N) \otimes_R N'$ as $(S \otimes_R N) \otimes_S (S \otimes_R N')$]
The module $S \otimes_R N$ is an $S$-module via the action $t \cdot (s \otimes n) = (ts) \otimes n$ (multiplication on the first factor), and $N'$ is an $R$-module. By the [Base Change for Extension of Scalars](/theorems/2916) (applied with the $S$-module $M := S \otimes_R N$ and the $R$-module $N'$), there is an $S$-module isomorphism
\begin{align*}
\beta: (S \otimes_R N) \otimes_R N' &\xrightarrow{\;\sim\;} (S \otimes_R N) \otimes_S (S \otimes_R N')
\end{align*}
sending $(s \otimes n) \otimes n' \mapsto (s \otimes n) \otimes (1_S \otimes n')$ on pure tensors.
[guided]
Why does the base change isomorphism apply here? The statement of the [Base Change for Extension of Scalars](/theorems/2916) gives an $S$-module isomorphism $M \otimes_R N' \cong M \otimes_S (S \otimes_R N')$ for any $S$-module $M$ and $R$-module $N'$. We set $M = S \otimes_R N$. The only hypothesis to verify is that $S \otimes_R N$ is an $S$-module, which it is: the $S$-action is $t \cdot (s \otimes n) = (ts) \otimes n$, defined via the $R$-bilinear map $S \times N \to S \otimes_R N$ and the $S$-module structure on $S$ (the first factor).
[/guided]
[/step]
[step:Compose the two isomorphisms and verify the formula on pure tensors]
Define the composite $S$-module isomorphism
\begin{align*}
\varphi := \beta \circ \alpha: S \otimes_R (N \otimes_R N') \xrightarrow{\;\sim\;} (S \otimes_R N) \otimes_S (S \otimes_R N').
\end{align*}
Since $\alpha$ and $\beta$ are both $S$-module isomorphisms, so is $\varphi$.
On a pure tensor $s \otimes (n \otimes n') \in S \otimes_R (N \otimes_R N')$:
\begin{align*}
\varphi(s \otimes (n \otimes n')) &= \beta(\alpha(s \otimes (n \otimes n'))) \\
&= \beta((s \otimes n) \otimes n') \\
&= (s \otimes n) \otimes (1_S \otimes n').
\end{align*}
We verify this matches the stated formula. The statement asserts $\varphi(s \otimes (n \otimes n')) = s \cdot ((1_S \otimes n) \otimes (1_S \otimes n'))$. Computing the right-hand side using the $S$-action on $(S \otimes_R N) \otimes_S (S \otimes_R N')$, which acts on the first factor of $S \otimes_R N$:
\begin{align*}
s \cdot ((1_S \otimes n) \otimes (1_S \otimes n')) = (s \cdot (1_S \otimes n)) \otimes (1_S \otimes n') = (s \otimes n) \otimes (1_S \otimes n').
\end{align*}
This equals $\varphi(s \otimes (n \otimes n'))$, confirming the formula.
[/step]
