[proofplan] We trace the vanishing of $\sum_{i=1}^\ell m_i \otimes n_i$ back to the explicit construction of the tensor product. The tensor product $M \otimes_R N$ is defined as a quotient $\mathcal{F} / K$, where $\mathcal{F}$ is the free $R$-module on the set $M \times N$ and $K$ is the submodule generated by the bilinearity relations. The hypothesis $\sum_i m_i \otimes n_i = 0$ means that a specific element of $\mathcal{F}$ lies in $K$, and expressing it as a finite $R$-linear combination of generators of $K$ involves only finitely many elements of $M$ and $N$. We take $M'$ and $N'$ to be the submodules generated by those finitely many elements, and observe that the same finite combination witnesses the vanishing in $M' \otimes_R N'$. [/proofplan] [step:Recall the construction of $M \otimes_R N$ as a quotient of a free module] Let $\mathcal{F} = R^{\oplus(M \times N)}$ denote the free $R$-module with basis $\{e_{(m,n)}\}_{(m,n) \in M \times N}$ indexed by the set $M \times N$. The tensor product $M \otimes_R N$ is defined as $\mathcal{F} / K$, where $K$ is the submodule of $\mathcal{F}$ generated by all elements of the following three forms: \begin{align*} &e_{(m_1 + m_2, n)} - e_{(m_1, n)} - e_{(m_2, n)}, \\ &e_{(m, n_1 + n_2)} - e_{(m, n_1)} - e_{(m, n_2)}, \\ &e_{(rm, n)} - e_{(m, rn)}, \end{align*} for all $m, m_1, m_2 \in M$, $n, n_1, n_2 \in N$, and $r \in R$. Under the quotient map $\pi: \mathcal{F} \to \mathcal{F}/K$, the image of $e_{(m,n)}$ is the pure tensor $m \otimes n$. [guided] The tensor product $M \otimes_R N$ is not defined abstractly --- it is built from a concrete construction. We start with the free $R$-module $\mathcal{F} = R^{\oplus(M \times N)}$, which has one formal basis element $e_{(m,n)}$ for each pair $(m,n) \in M \times N$. This is a very large module (one generator per pair), but it lets us track exactly which elements of $M$ and $N$ participate in any given relation. The tensor product is the quotient $\mathcal{F}/K$, where $K$ is generated by three families of relations encoding bilinearity and $R$-balance: \begin{align*} &e_{(m_1 + m_2, n)} - e_{(m_1, n)} - e_{(m_2, n)}, \\ &e_{(m, n_1 + n_2)} - e_{(m, n_1)} - e_{(m, n_2)}, \\ &e_{(rm, n)} - e_{(m, rn)}, \end{align*} for all $m, m_1, m_2 \in M$, $n, n_1, n_2 \in N$, and $r \in R$. The quotient map $\pi: \mathcal{F} \to \mathcal{F}/K$ sends $e_{(m,n)}$ to the pure tensor $m \otimes n$. The key point for what follows is that each individual generator of $K$ involves only finitely many elements of $M$ and $N$. [/guided] [/step] [step:Express the vanishing hypothesis as a finite linear combination of generators of $K$] The hypothesis $\sum_{i=1}^\ell m_i \otimes n_i = 0$ in $M \otimes_R N$ means that the element $\sum_{i=1}^\ell e_{(m_i, n_i)}$ lies in $K$. Since $K$ is generated by elements of the three forms above, there exist finitely many scalars $r_j \in R$ and finitely many generators $k_j$ of $K$ (each of one of the three types) such that \begin{align*} \sum_{i=1}^\ell e_{(m_i, n_i)} = \sum_{j=1}^s r_j k_j. \end{align*} Each generator $k_j$ involves at most three elements of $M$ and at most three elements of $N$ (appearing as indices of the basis elements $e_{(\cdot, \cdot)}$). Since the sum is finite, only finitely many elements of $M$ and $N$ appear across all the generators $k_1, \ldots, k_s$. [guided] What does $\sum_{i=1}^\ell m_i \otimes n_i = 0$ mean at the level of the free module? By definition, $m_i \otimes n_i = \pi(e_{(m_i, n_i)})$, so the vanishing condition is $\pi\left(\sum_{i=1}^\ell e_{(m_i, n_i)}\right) = 0$, i.e., $\sum_{i=1}^\ell e_{(m_i, n_i)} \in K$. Now $K$ is generated as an $R$-module by elements of the three bilinearity/balance forms. Any element of $K$ is therefore a finite $R$-linear combination of such generators. So there exist $r_1, \ldots, r_s \in R$ and generators $k_1, \ldots, k_s$ of $K$ such that \begin{align*} \sum_{i=1}^\ell e_{(m_i, n_i)} = \sum_{j=1}^s r_j k_j. \end{align*} Each generator $k_j$ is one of the three types: for instance, $e_{(m_1'+m_2', n')} - e_{(m_1', n')} - e_{(m_2', n')}$ involves the elements $m_1', m_2', m_1'+m_2' \in M$ and $n' \in N$. The crucial observation is that this expression is a **finite** sum, so only finitely many elements of $M$ and of $N$ appear as indices across all the generators $k_1, \ldots, k_s$. [/guided] [/step] [step:Define $M'$ and $N'$ to contain all elements appearing in the finite combination] Let $m_1', \ldots, m_r' \in M$ be all the elements of $M$ that appear as indices in the generators $k_1, \ldots, k_s$ (including sums $m_a + m_b$ and scalar multiples $rm_a$ that appear). Similarly, let $n_1', \ldots, n_t' \in N$ be all elements of $N$ appearing as indices. Define \begin{align*} M' &:= \text{the submodule of } M \text{ generated by } \{m_1, \ldots, m_\ell, m_1', \ldots, m_r'\}, \\ N' &:= \text{the submodule of } N \text{ generated by } \{n_1, \ldots, n_\ell, n_1', \ldots, n_t'\}. \end{align*} Both $M'$ and $N'$ are finitely generated submodules. By construction, $m_i \in M'$ for all $1 \leq i \leq \ell$ and $n_i \in N'$ for all $1 \leq i \leq \ell$. [guided] We now collect all the elements of $M$ and $N$ that were "used" in the finite expression $\sum_j r_j k_j$. Let $m_1', \ldots, m_r'$ be every element of $M$ appearing as an index in any of the generators $k_1, \ldots, k_s$, and let $n_1', \ldots, n_t'$ be every element of $N$ appearing as an index. We define \begin{align*} M' &:= \text{the submodule of } M \text{ generated by } \{m_1, \ldots, m_\ell, m_1', \ldots, m_r'\}, \\ N' &:= \text{the submodule of } N \text{ generated by } \{n_1, \ldots, n_\ell, n_1', \ldots, n_t'\}. \end{align*} We include $m_1, \ldots, m_\ell$ and $n_1, \ldots, n_\ell$ to ensure the original pure tensors $m_i \otimes n_i$ make sense in $M' \otimes_R N'$. Both $M'$ and $N'$ are finitely generated by construction, since each is generated by a finite set of elements. [/guided] [/step] [step:Verify that the same combination witnesses vanishing in $M' \otimes_R N'$] Consider the tensor product $M' \otimes_R N'$, constructed as $\mathcal{F}' / K'$, where $\mathcal{F}' = R^{\oplus(M' \times N')}$ and $K'$ is the submodule of $\mathcal{F}'$ generated by the bilinearity relations for $M' \times N'$. Since every element of $M$ and $N$ appearing in the generators $k_1, \ldots, k_s$ belongs to $M'$ and $N'$ respectively, each generator $k_j$ --- originally a bilinearity relation in $\mathcal{F}$ --- restricts to a bilinearity relation in $\mathcal{F}'$, and hence lies in $K'$ when viewed as an element of $\mathcal{F}'$. The same finite combination \begin{align*} \sum_{i=1}^\ell e_{(m_i, n_i)} = \sum_{j=1}^s r_j k_j \end{align*} is therefore a valid identity in $\mathcal{F}'$, with the right-hand side in $K'$. This means $\sum_{i=1}^\ell e_{(m_i, n_i)} \in K'$, i.e., $\sum_{i=1}^\ell m_i \otimes n_i = 0$ in $M' \otimes_R N'$. [guided] Now we need to check that the finite combination witnessing $\sum_i m_i \otimes n_i = 0$ in $M \otimes_R N$ also witnesses the same vanishing in the smaller tensor product $M' \otimes_R N'$. The tensor product $M' \otimes_R N'$ is constructed identically: $\mathcal{F}' = R^{\oplus(M' \times N')}$ with submodule $K'$ generated by bilinearity relations for pairs in $M' \times N'$. The inclusion $M' \subseteq M$, $N' \subseteq N$ induces an inclusion $M' \times N' \subseteq M \times N$, and hence $\mathcal{F}'$ embeds into $\mathcal{F}$ (as the submodule spanned by basis elements $e_{(m',n')}$ with $m' \in M'$, $n' \in N'$). Each generator $k_j$ in our finite combination is a bilinearity relation involving elements that all lie in $M'$ and $N'$ by construction. For instance, if $k_j = e_{(m_a'+m_b', n')} - e_{(m_a', n')} - e_{(m_b', n')}$, then $m_a', m_b', m_a'+m_b' \in M'$ (since $M'$ is a submodule and hence closed under addition) and $n' \in N'$. So $k_j$ is a bilinearity relation for $M' \times N'$, meaning $k_j \in K'$. Therefore $\sum_{i=1}^\ell e_{(m_i, n_i)} = \sum_{j=1}^s r_j k_j \in K'$, which gives $\sum_{i=1}^\ell m_i \otimes n_i = 0$ in $M' \otimes_R N'$. [/guided] [/step]