[proofplan] We use the standard definition of a basis of a left module as a family for which every module element has a unique expression as a finite $R$-linear combination of the family. In the forward direction, uniqueness of finite coordinates gives both existence of such expressions and the absence of nonzero finite linear relations. In the reverse direction, spanning gives existence of finite expressions, while [linear independence](/page/Linear%20Independence) proves uniqueness by subtracting two proposed expressions. [/proofplan]

[step:Unfold the finite-coordinate definition of a basis] For this proof, an expression of an element $m \in M$ in the family $(e_i)_{i \in I}$ means a choice of a finite subset $F \subset I$ and coefficients $(r_i)_{i \in F}$ in $R$ such that \begin{align*} m = \sum_{i \in F} r_i e_i. \end{align*} The family $(e_i)_{i \in I}$ is a basis of $M$ precisely when every $m \in M$ admits exactly one such finite expression, after the usual convention that coefficients outside the chosen finite support are zero. [/step]

[step:Derive spanning and independence from uniqueness of finite expressions] Assume that $(e_i)_{i \in I}$ is a basis of $M$. By the definition just stated, every $m \in M$ has a finite expression as an $R$-linear combination of the elements $e_i$, so the family spans $M$. It remains to prove $R$-linear independence. Let $F \subset I$ be finite, and let $(r_i)_{i \in F}$ be coefficients in $R$ such that \begin{align*} \sum_{i \in F} r_i e_i = 0_M. \end{align*} The element $0_M$ also has the finite expression with the same support $F$ and all coefficients equal to $0_R$: \begin{align*} 0_M = \sum_{i \in F} 0_R e_i. \end{align*} Since the basis expression of $0_M$ is unique, the two coefficient families agree on $F$. Hence $r_i = 0_R$ for every $i \in F$, which is exactly $R$-linear independence. [/step]

[step:Use spanning and independence to prove uniqueness of finite expressions]Conversely, assume that $(e_i)_{i \in I}$ spans $M$ and is $R$-linearly independent. Spanning gives existence of a finite expression for every $m \in M$. We prove uniqueness. Let $m \in M$, and suppose that $m$ has two finite expressions. Thus there exist finite subsets $F, G \subset I$ and coefficient families $(r_i)_{i \in F}$ and $(s_i)_{i \in G}$ in $R$ such that \begin{align*} m = \sum_{i \in F} r_i e_i. \end{align*} and \begin{align*} m = \sum_{i \in G} s_i e_i. \end{align*} Define $H := F \cup G$, which is finite. Extend the coefficients to $H$ by setting $r_i := 0_R$ for $i \in H \setminus F$ and $s_i := 0_R$ for $i \in H \setminus G$. Subtracting the two displayed expressions in the left $R$-module $M$ gives \begin{align*} 0_M = \sum_{i \in H} (r_i - s_i)e_i. \end{align*} By $R$-linear independence, $r_i - s_i = 0_R$ for every $i \in H$. Hence $r_i = s_i$ for every $i \in H$, so the two finite expressions agree after extension by zero. Therefore every $m \in M$ has a unique finite expression.[/step]

[guided]We already know that spanning gives at least one expression for each $m \in M$. The only remaining point in the definition of a basis is uniqueness. So fix an element $m \in M$ and suppose that two finite expressions have been given: \begin{align*} m = \sum_{i \in F} r_i e_i. \end{align*} and \begin{align*} m = \sum_{i \in G} s_i e_i. \end{align*} Here $F \subset I$ and $G \subset I$ are finite, while $(r_i)_{i \in F}$ and $(s_i)_{i \in G}$ are families of coefficients in $R$. To compare the two expressions coefficient by coefficient, we first put them on the same finite index set. Define $H := F \cup G$. Since $F$ and $G$ are finite, $H$ is finite. Extend the first coefficient family to $H$ by setting $r_i := 0_R$ for every $i \in H \setminus F$, and extend the second coefficient family to $H$ by setting $s_i := 0_R$ for every $i \in H \setminus G$. These extensions do not change either finite sum, because the new terms have coefficient $0_R$. Now subtract the second expression for $m$ from the first expression for $m$. Since $M$ is a left $R$-module, finite sums may be added and subtracted termwise, and distributivity gives \begin{align*} 0_M = m - m = \sum_{i \in H} (r_i - s_i)e_i. \end{align*} This is a finite $R$-linear relation among the family $(e_i)_{i \in I}$. The assumed $R$-linear independence says that every coefficient in such a relation must be zero. Therefore $r_i - s_i = 0_R$ for every $i \in H$, and hence $r_i = s_i$ for every $i \in H$. Thus the two expressions agree after both are viewed as coefficient families on the common finite support $H$. This proves uniqueness of finite expressions for the chosen element $m$. Since $m \in M$ was arbitrary, every element of $M$ has a unique finite expression as an $R$-linear combination of the family.[/guided]

[step:Conclude the equivalence] The forward direction proves that every basis spans and is $R$-linearly independent. The reverse direction proves that every spanning and $R$-linearly independent family gives unique finite expressions for all elements of $M$, hence is a basis. Therefore $(e_i)_{i \in I}$ is a basis of $M$ if and only if it spans $M$ and is $R$-linearly independent. [/step]