[proofplan]
Let $A:=R\times S$ and use the two central idempotents $e_R=(1_R,0_S)$ and $e_S=(0_R,1_S)$. These idempotents decompose every left $A$-module into its $R$-part and its $S$-part, and this decomposition preserves finite generation, projectivity, and direct sums; passing to the Grothendieck group gives the $K_0$ decomposition. For $K_1$, the entrywise identification $M_n(A)\cong M_n(R)\times M_n(S)$ identifies general linear groups and elementary subgroups compatibly with stabilization, so the [stable Whitehead quotient](/theorems/8654) splits as the product, equivalently the direct sum, of the two factors.
[/proofplan]
[step:Decompose modules over $R\times S$ using the product idempotents]
Put $A:=R\times S$, and define
\begin{align*}
e_R:=(1_R,0_S)\in A
\end{align*}
and
\begin{align*}
e_S:=(0_R,1_S)\in A.
\end{align*}
Then $e_R^2=e_R$, $e_S^2=e_S$, $e_Re_S=0_A$, and $e_R+e_S=1_A$.
Let $M$ be a left $A$-module. Define
\begin{align*}
M_R:=e_RM
\end{align*}
and
\begin{align*}
M_S:=e_SM.
\end{align*}
The abelian group $M_R$ is a left $R$-module by
\begin{align*}
r\cdot m:=(r,0_S)m
\end{align*}
for $r\in R$ and $m\in M_R$, and $M_S$ is a left $S$-module by
\begin{align*}
s\cdot m:=(0_R,s)m
\end{align*}
for $s\in S$ and $m\in M_S$.
The map
\begin{align*}
\Phi_M:M_R\oplus M_S&\to M
\end{align*}
defined by
\begin{align*}
\Phi_M(m_R,m_S)=m_R+m_S
\end{align*}
is an isomorphism of left $A$-modules, where $A$ acts on $M_R\oplus M_S$ by
\begin{align*}
(r,s)\cdot(m_R,m_S)=(r\cdot m_R,s\cdot m_S).
\end{align*}
Indeed, for every $m\in M$,
\begin{align*}
m=1_Am=(e_R+e_S)m=e_Rm+e_Sm,
\end{align*}
so $\Phi_M$ is surjective. If $m_R+m_S=0$ with $m_R\in M_R$ and $m_S\in M_S$, then applying $e_R$ gives $m_R=0$, and applying $e_S$ gives $m_S=0$, so $\Phi_M$ is injective. The compatibility with the $A$-action follows from the identities $e_R(r,s)=(r,0_S)$ and $e_S(r,s)=(0_R,s)$.
Conversely, if $P$ is a left $R$-module and $Q$ is a left $S$-module, define the left $A$-module
\begin{align*}
P\boxplus Q:=P\oplus Q
\end{align*}
by
\begin{align*}
(r,s)\cdot(p,q)=(rp,sq).
\end{align*}
The preceding construction sends $P\boxplus Q$ back to the pair $(P,Q)$ through the identifications $e_R(P\boxplus Q)\cong P$ and $e_S(P\boxplus Q)\cong Q$. Thus left $A$-modules are identified with pairs consisting of a left $R$-module and a left $S$-module. This is precisely the product-ring module decomposition proved in [[Module Categories over a Product Ring](/theorems/8635)][citetheorem:8635].
[guided]
The reason the product ring splits modules is that $A=R\times S$ contains two complementary projectors. We define
\begin{align*}
e_R:=(1_R,0_S)
\end{align*}
and
\begin{align*}
e_S:=(0_R,1_S).
\end{align*}
They satisfy
\begin{align*}
e_R^2=e_R,\qquad e_S^2=e_S,\qquad e_Re_S=0_A,\qquad e_R+e_S=1_A.
\end{align*}
Thus $e_R$ extracts the $R$-component of an $A$-module and $e_S$ extracts the $S$-component.
Let $M$ be a left $A$-module. We define
\begin{align*}
M_R:=e_RM
\end{align*}
and
\begin{align*}
M_S:=e_SM.
\end{align*}
The set $M_R$ becomes a left $R$-module by the rule
\begin{align*}
r\cdot m:=(r,0_S)m
\end{align*}
for $r\in R$ and $m\in M_R$. Similarly, $M_S$ becomes a left $S$-module by
\begin{align*}
s\cdot m:=(0_R,s)m.
\end{align*}
These definitions are legitimate because $(r,0_S)e_R=(r,0_S)$ and $(0_R,s)e_S=(0_R,s)$, so the action stays inside the corresponding summand.
Now define
\begin{align*}
\Phi_M:M_R\oplus M_S&\to M
\end{align*}
by
\begin{align*}
\Phi_M(m_R,m_S)=m_R+m_S.
\end{align*}
This map is surjective because every element $m\in M$ decomposes as
\begin{align*}
m=1_Am=(e_R+e_S)m=e_Rm+e_Sm,
\end{align*}
with $e_Rm\in M_R$ and $e_Sm\in M_S$. It is injective because if $m_R+m_S=0$, then applying $e_R$ gives
\begin{align*}
0=e_R(m_R+m_S)=e_Rm_R+e_Rm_S=m_R+0=m_R,
\end{align*}
and applying $e_S$ gives $m_S=0$. Finally, it is $A$-linear because for $(r,s)\in A$,
\begin{align*}
\Phi_M((r,s)\cdot(m_R,m_S))=rm_R+sm_S
\end{align*}
where $rm_R$ means $(r,0_S)m_R$ and $sm_S$ means $(0_R,s)m_S$, while
\begin{align*}
(r,s)\Phi_M(m_R,m_S)=(r,s)(m_R+m_S)=(r,0_S)m_R+(0_R,s)m_S.
\end{align*}
Thus $\Phi_M$ is an $A$-module isomorphism.
Conversely, from a left $R$-module $P$ and a left $S$-module $Q$, we build a left $A$-module
\begin{align*}
P\boxplus Q:=P\oplus Q
\end{align*}
with action
\begin{align*}
(r,s)\cdot(p,q)=(rp,sq).
\end{align*}
Applying the [idempotent decomposition](/theorems/446) to $P\boxplus Q$ recovers $P$ and $Q$. This is exactly the equivalence of module categories over a product ring stated in [Module Categories over a Product Ring][citetheorem:8635].
[/guided]
[/step]
[step:Restrict the decomposition to finitely generated projective modules]
Let $\operatorname{Proj}(T)$ denote the class of finitely generated projective left modules over a unital ring $T$.
If $M\in\operatorname{Proj}(A)$, then there exist an integer $n\geq 0$ and a left $A$-module $N$ such that
\begin{align*}
M\oplus N\cong A^n
\end{align*}
as left $A$-modules. Applying $e_R$ gives
\begin{align*}
M_R\oplus N_R\cong e_RA^n\cong R^n
\end{align*}
as left $R$-modules, so $M_R$ is finitely generated projective over $R$. Similarly,
\begin{align*}
M_S\oplus N_S\cong e_SA^n\cong S^n,
\end{align*}
so $M_S$ is finitely generated projective over $S$.
Conversely, suppose $P\in\operatorname{Proj}(R)$ and $Q\in\operatorname{Proj}(S)$. Choose integers $m,n\geq 0$ and modules $P'$ over $R$ and $Q'$ over $S$ such that
\begin{align*}
P\oplus P'\cong R^m
\end{align*}
and
\begin{align*}
Q\oplus Q'\cong S^n.
\end{align*}
Then
\begin{align*}
(P\boxplus Q)\oplus(P'\boxplus Q')\cong R^m\boxplus S^n.
\end{align*}
The module $R^m\boxplus S^n$ is finitely generated projective over $A$ because it is a direct summand of
\begin{align*}
A^{m+n}\cong (R^{m+n})\boxplus(S^{m+n}).
\end{align*}
Therefore $P\boxplus Q$ is finitely generated projective over $A$.
[/step]
[step:Pass from projective modules to the $K_0$ group]
Let $V(T)$ denote the commutative monoid of isomorphism classes of finitely generated projective left $T$-modules under direct sum. Define
\begin{align*}
\Theta_0:V(A)&\to V(R)\oplus V(S)
\end{align*}
by
\begin{align*}
\Theta_0([M])=([M_R],[M_S]).
\end{align*}
The previous step shows that this map is well-defined. Its inverse is the monoid homomorphism
\begin{align*}
\Psi_0:V(R)\oplus V(S)&\to V(A)
\end{align*}
defined by
\begin{align*}
\Psi_0([P],[Q])=[P\boxplus Q].
\end{align*}
The identities $\Theta_0\Psi_0=\operatorname{id}_{V(R)\oplus V(S)}$ and $\Psi_0\Theta_0=\operatorname{id}_{V(A)}$ follow from the decomposition $M\cong M_R\boxplus M_S$. Hence
\begin{align*}
V(A)\cong V(R)\oplus V(S)
\end{align*}
as commutative monoids.
By definition, $K_0(T)$ is the Grothendieck group completion of $V(T)$. Group completion sends this monoid isomorphism to an isomorphism of abelian groups:
\begin{align*}
K_0(R\times S)=K_0(A)\cong K_0(R)\oplus K_0(S).
\end{align*}
This proves the $K_0$ decomposition.
[/step]
[step:Identify stable general linear groups over the product ring]
For each integer $n\geq 1$, define
\begin{align*}
\alpha_n:M_n(A)&\to M_n(R)\times M_n(S)
\end{align*}
by applying the two coordinate projections $A\to R$ and $A\to S$ to every matrix entry. This is a ring isomorphism, with inverse sending a pair of matrices $(B,C)$ to the matrix whose $(i,j)$-entry is $(B_{ij},C_{ij})$.
Restricting to units gives a group isomorphism
\begin{align*}
\beta_n:GL_n(A)&\to GL_n(R)\times GL_n(S).
\end{align*}
The stabilization homomorphism $GL_n(T)\to GL_{n+1}(T)$ for a unital ring $T$ sends a matrix $X$ to $\operatorname{diag}(X,1_T)$. If $X\in GL_n(A)$ and $\alpha_n(X)=(X_R,X_S)$ with $X_R\in GL_n(R)$ and $X_S\in GL_n(S)$, then
\begin{align*}
\alpha_{n+1}(\operatorname{diag}(X,1_A))=(\operatorname{diag}(X_R,1_R),\operatorname{diag}(X_S,1_S)).
\end{align*}
Thus the maps $\beta_n$ are compatible with stabilization. Passing to the direct limit gives a group isomorphism
\begin{align*}
\beta:GL(A)&\to GL(R)\times GL(S).
\end{align*}
For $n\geq 2$, $1\leq i\ne j\leq n$, and $t\in T$ in a unital ring $T$, let $E_{ij,n}\in M_n(T)$ denote the matrix unit with $1_T$ in the $(i,j)$-entry and $0_T$ elsewhere, and define the elementary transvection
\begin{align*}
e_{ij,n}(t):=I_n+tE_{ij,n}\in GL_n(T).
\end{align*}
For $(r,s)\in A$, the elementary transvection $e_{ij,n}((r,s))\in GL_n(A)$ maps to
\begin{align*}
(e_{ij,n}(r),e_{ij,n}(s))\in GL_n(R)\times GL_n(S).
\end{align*}
Hence $\beta(E(A))\subset E(R)\times E(S)$. Conversely, for $r\in R$ and $s\in S$, the elements $(e_{ij,n}(r),I_n)$ and $(I_n,e_{ij,n}(s))$ are respectively the images under $\beta_n$ of $e_{ij,n}((r,0_S))$ and $e_{ij,n}((0_R,s))$. Since the elementary transvections generate $E(R)$ and $E(S)$ after stabilization, these two families generate $E(R)\times E(S)$. Thus $\beta$ carries the stable elementary subgroup $E(A)$ onto $E(R)\times E(S)$.
[/step]
[step:Pass to the Whitehead quotient and obtain the $K_1$ decomposition]
By [[Stable Elementary Subgroup Is Normal](/theorems/8655)][citetheorem:8655], $E(A)\trianglelefteq GL(A)$, $E(R)\trianglelefteq GL(R)$, and $E(S)\trianglelefteq GL(S)$. Therefore $E(R)\times E(S)$ is a [normal subgroup](/page/Normal%20Subgroup) of $GL(R)\times GL(S)$, and the isomorphism $\beta:GL(A)\to GL(R)\times GL(S)$ induces an isomorphism of quotient groups
\begin{align*}
GL(A)/E(A)\cong (GL(R)\times GL(S))/(E(R)\times E(S)).
\end{align*}
The map
\begin{align*}
(GL(R)\times GL(S))/(E(R)\times E(S))&\to GL(R)/E(R)\times GL(S)/E(S)
\end{align*}
defined by
\begin{align*}
[(g,h)]\mapsto ([g],[h])
\end{align*}
is a well-defined group isomorphism, because equality modulo $E(R)\times E(S)$ is exactly equality modulo $E(R)$ in the first coordinate and modulo $E(S)$ in the second coordinate.
Using the definition $K_1(T)=GL(T)/E(T)$, we obtain
\begin{align*}
K_1(R\times S)=K_1(A)\cong K_1(R)\times K_1(S).
\end{align*}
By the [Stable Whitehead Quotient][citetheorem:8654], $K_1(T)$ is abelian for every unital ring $T$, so the finite product of the two abelian groups is canonically the same as their direct sum. Therefore
\begin{align*}
K_1(R\times S)\cong K_1(R)\oplus K_1(S).
\end{align*}
Together with the $K_0$ decomposition proved above, this gives the two claimed canonical isomorphisms.
[/step]
