[proofplan]
We prove invariant basis number by reducing an isomorphism of finite free $R$-modules to an isomorphism of finite-dimensional vector spaces. Since $R$ is nonzero, it has a maximal ideal $\mathfrak m$, and the residue ring $k=R/\mathfrak m$ is a field. Tensoring an assumed isomorphism $R^m\cong R^n$ with $k$ over $R$ gives an isomorphism $k^m\cong k^n$, and invariance of vector-space dimension then forces $m=n$.
[/proofplan]
[step:Choose a residue field of the nonzero ring]
Let $R$ be a nonzero commutative unital ring. By the standard maximal ideal theorem for nonzero commutative unital rings, there exists a maximal ideal $\mathfrak m\trianglelefteq R$. Define the [quotient ring](/page/Quotient%20Ring)
\begin{align*}
k := R/\mathfrak m.
\end{align*}
Since $\mathfrak m$ is maximal, the standard quotient criterion for maximal ideals implies that $k$ is a field. Let
\begin{align*}
\pi:R\to k
\end{align*}
be the quotient homomorphism. We regard $k$ as a left $R$-module through $\pi$, so that $r\cdot a=\pi(r)a$ for $r\in R$ and $a\in k$.
[/step]
[step:Tensor an arbitrary free-module isomorphism with the residue field]
Let $m,n\geq 0$ be integers, and suppose that
\begin{align*}
\Phi:R^m\to R^n
\end{align*}
is an isomorphism of left $R$-modules. Define the induced map
\begin{align*}
\operatorname{id}_k\otimes_R \Phi:k\otimes_R R^m\to k\otimes_R R^n
\end{align*}
by
\begin{align*}
a\otimes x\mapsto a\otimes \Phi(x).
\end{align*}
This map is an isomorphism, with inverse $\operatorname{id}_k\otimes_R \Phi^{-1}$, because [tensor product](/page/Tensor%20Product) over $R$ is functorial and preserves inverse pairs of maps.
[guided]
We start with the precise object whose rank we want to test. Let $m,n\geq 0$ be integers, and assume that
\begin{align*}
\Phi:R^m\to R^n
\end{align*}
is an isomorphism of left $R$-modules. To compare $m$ and $n$, we pass from modules over $R$ to vector spaces over the field $k=R/\mathfrak m$.
The passage is made by tensoring over $R$ with the left $R$-module $k$. Define
\begin{align*}
\operatorname{id}_k\otimes_R \Phi:k\otimes_R R^m\to k\otimes_R R^n
\end{align*}
on pure tensors by
\begin{align*}
a\otimes x\mapsto a\otimes \Phi(x).
\end{align*}
This formula is well-defined by the [universal property of the tensor product](/theorems/3971), since the assignment $(a,x)\mapsto a\otimes \Phi(x)$ is $R$-balanced.
Now we verify that the induced map is an isomorphism rather than merely a homomorphism. Since $\Phi$ is an isomorphism, it has an $R$-linear inverse
\begin{align*}
\Phi^{-1}:R^n\to R^m.
\end{align*}
Functoriality of tensor product gives maps $\operatorname{id}_k\otimes_R\Phi$ and $\operatorname{id}_k\otimes_R\Phi^{-1}$. Their composites are
\begin{align*}
(\operatorname{id}_k\otimes_R\Phi^{-1})\circ(\operatorname{id}_k\otimes_R\Phi)
=
\operatorname{id}_k\otimes_R(\Phi^{-1}\circ\Phi)
=
\operatorname{id}_k\otimes_R\operatorname{id}_{R^m}
=
\operatorname{id}_{k\otimes_R R^m}.
\end{align*}
Similarly,
\begin{align*}
(\operatorname{id}_k\otimes_R\Phi)\circ(\operatorname{id}_k\otimes_R\Phi^{-1})
=
\operatorname{id}_{k\otimes_R R^n}.
\end{align*}
Therefore $\operatorname{id}_k\otimes_R\Phi$ is an isomorphism with inverse $\operatorname{id}_k\otimes_R\Phi^{-1}$.
[/guided]
[/step]
[step:Identify the tensor products with finite-dimensional vector spaces]
For every integer $q\geq 0$, define the $k$-[linear map](/page/Linear%20Map)
\begin{align*}
\Theta_q:k\otimes_R R^q\to k^q
\end{align*}
by
\begin{align*}
a\otimes (r_1,\dots,r_q)\mapsto (a\pi(r_1),\dots,a\pi(r_q)).
\end{align*}
This is the standard base-change isomorphism for finite free modules, with inverse sending the $i$-th standard basis vector of $k^q$ to $1_k\otimes e_i$, where $e_i$ is the $i$-th standard basis vector of $R^q$. Hence
\begin{align*}
k\otimes_R R^m\cong k^m
\end{align*}
and
\begin{align*}
k\otimes_R R^n\cong k^n.
\end{align*}
Combining these identifications with $\operatorname{id}_k\otimes_R\Phi$, we obtain an isomorphism of $k$-vector spaces
\begin{align*}
k^m\cong k^n.
\end{align*}
[/step]
[step:Compare vector-space dimensions to recover the ranks]
Since $k$ is a field, $k^m$ and $k^n$ are finite-dimensional vector spaces over $k$. Their dimensions are
\begin{align*}
\dim_k(k^m)=m
\end{align*}
and
\begin{align*}
\dim_k(k^n)=n.
\end{align*}
Isomorphic finite-dimensional vector spaces over a field have the same dimension, so the isomorphism $k^m\cong k^n$ gives
\begin{align*}
m=n.
\end{align*}
Thus every isomorphism $R^m\cong R^n$ of finite free left $R$-modules has $m=n$, and therefore $R$ has invariant basis number.
[/step]
