[proofplan]
We regard $R[t]$ as the coordinate ring of the affine line over $\operatorname{Spec}(R)$. Quillen's homotopy invariance theorem for regular Noetherian schemes says that pullback along the affine-line projection induces isomorphisms on algebraic K-groups. In the affine case this pullback is exactly the map induced by the inclusion $i:R\to R[t]$. Finally, evaluation at $t=0$ gives a ring homomorphism $R[t]\to R$ whose composite with $i$ is the identity, so functoriality identifies the evaluation map as the inverse.
[/proofplan]
[step:Identify the polynomial extension with the affine-line projection]
Let $X := \operatorname{Spec}(R)$ and $Y := \operatorname{Spec}(R[t])$.
Since $R$ is Noetherian, $X$ is a Noetherian affine scheme. By the hypothesis in the formalized statement, for every prime ideal $\mathfrak p\in\operatorname{Spec}(R)$ the local ring $R_{\mathfrak p}$ is regular. Since $\mathcal O_{X,\mathfrak p}=R_{\mathfrak p}$ for the affine scheme $X=\operatorname{Spec}(R)$, every local ring of $X$ is regular, so $X$ is a regular Noetherian scheme.
Define the affine line over $\operatorname{Spec}(\mathbb Z)$ to be the scheme $\mathbb A^1_{\mathbb Z} := \operatorname{Spec}(\mathbb Z[t])$. For the scheme $X$, define $\mathbb A^1_X := X\times_{\operatorname{Spec}(\mathbb Z)}\mathbb A^1_{\mathbb Z}$.
The unital inclusion $i:R\to R[t]$ corresponds contravariantly to the affine-line projection $p:Y=\operatorname{Spec}(R[t])\to X=\operatorname{Spec}(R)$.
Equivalently, $Y$ is canonically isomorphic to $\mathbb A^1_X$ over $X$, and $p$ is the projection onto $X$.
[/step]
[step:Apply Quillen homotopy invariance to the affine line over $\operatorname{Spec}(R)$]
For a scheme $Z$, write $K_n(Z)$ for its Quillen algebraic K-group. We use Quillen's homotopy invariance theorem for regular Noetherian schemes: if $Z$ is a regular Noetherian scheme and $p:\mathbb A^1_Z \to Z$ is the affine-line projection, then for every integer $n\ge 0$ the pullback map $p^*:K_n(Z)\to K_n(\mathbb A^1_Z)$ is an isomorphism. This is the standard Quillen homotopy invariance theorem, proved using the localization sequence in algebraic K-theory, Noetherian induction on closed subsets, and dévissage for the regular closed pieces.
The hypotheses of this theorem are satisfied by the preceding step: $X=\operatorname{Spec}(R)$ is regular and Noetherian. Therefore $p^*:K_0(X)\to K_0(Y)$ and $p^*:K_1(X)\to K_1(Y)$ are isomorphisms.
For every commutative unital ring $A$, Quillen K-theory of $\operatorname{Spec}(A)$ agrees with Quillen algebraic K-theory of $A$. Applying this with $A=R$ and $A=R[t]$, under the identifications
\begin{align*}
K_n(X)=K_n(R)
\end{align*}
and
\begin{align*}
K_n(Y)=K_n(R[t]),
\end{align*}
the pullback $p^*$ is the extension-of-scalars map induced by $i:R\to R[t]$, namely $K_n(i)$. Hence $K_0(i)$ and $K_1(i)$ are isomorphisms.
[guided]
For a scheme $Z$, write $K_n(Z)$ for its Quillen algebraic K-group, and write $\mathbb A^1_Z := Z\times_{\operatorname{Spec}(\mathbb Z)}\operatorname{Spec}(\mathbb Z[t])$ for the affine line over $Z$. The point of the argument is that the [polynomial ring](/page/Polynomial%20Ring) $R[t]$ is not being treated by elementary manipulation of projective modules or matrices. Instead, it is treated geometrically as the affine line over $\operatorname{Spec}(R)$.
We use the following external theorem, Quillen's homotopy invariance theorem for regular Noetherian schemes: if $X$ is a regular Noetherian scheme and
\begin{align*}
p:\mathbb A^1_X\to X
\end{align*}
is the affine-line projection, then for every integer $n\ge 0$ the pullback
\begin{align*}
p^*:K_n(X)\to K_n(\mathbb A^1_X)
\end{align*}
is an isomorphism. Its standard proof uses Quillen's localization sequence, Noetherian induction, and dévissage; regularity is the hypothesis ensuring that the coherent sheaves that appear are controlled by finite locally free resolutions.
Now verify the hypotheses. We have set $X=\operatorname{Spec}(R)$. Since $R$ is Noetherian, $X$ is Noetherian. Since $R$ is regular, all local rings of $X$ are regular local rings, so $X$ is regular. The preceding step identifies $\operatorname{Spec}(R[t])$ with $\mathbb A^1_X=X\times_{\operatorname{Spec}(\mathbb Z)}\operatorname{Spec}(\mathbb Z[t])$ over $X$, and under this identification the morphism induced by $i:R\to R[t]$ is the affine-line projection. Thus Quillen homotopy invariance applies to the projection
\begin{align*}
p:\operatorname{Spec}(R[t])\to\operatorname{Spec}(R).
\end{align*}
It gives isomorphisms
\begin{align*}
p^*:K_0(\operatorname{Spec}(R))\to K_0(\operatorname{Spec}(R[t]))
\end{align*}
and
\begin{align*}
p^*:K_1(\operatorname{Spec}(R))\to K_1(\operatorname{Spec}(R[t])).
\end{align*}
Finally we translate this back to rings. For an affine scheme $\operatorname{Spec}(A)$, Quillen K-theory of the scheme is the same as Quillen algebraic K-theory of the ring $A$. The morphism $p$ is the scheme morphism corresponding to the ring homomorphism
\begin{align*}
i:R\to R[t].
\end{align*}
Therefore the pullback $p^*$ is exactly the induced map
\begin{align*}
K_n(i):K_n(R)\to K_n(R[t]).
\end{align*}
Taking $n=0$ and $n=1$ gives that $K_0(i)$ and $K_1(i)$ are isomorphisms.
[/guided]
[/step]
[step:Use evaluation at $t=0$ to identify the inverse map]
Define the evaluation homomorphism $\varepsilon:R[t]\to R$ by $\varepsilon(f(t)) = f(0)$ for a polynomial $f(t)\in R[t]$. Then $\varepsilon\circ i = \operatorname{id}_R$. By [functoriality of low algebraic K-groups](/theorems/8627), for each $n\in\{0,1\}$ we have $K_n(\varepsilon)\circ K_n(i) = K_n(\varepsilon\circ i) = K_n(\operatorname{id}_R) = \operatorname{id}_{K_n(R)}$. Since $K_n(i)$ is an isomorphism by the preceding step, this left inverse is its two-sided inverse. Hence $K_n(i)\circ K_n(\varepsilon) = \operatorname{id}_{K_n(R[t])}$ for $n=0,1$. Therefore $K_0(i)$ and $K_1(i)$ are isomorphisms, as claimed.
[/step]
