Proof of The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums and Products

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Throughout, $x,y,z$ range over $R$, and we use the identities of Commutative Rings §ring: $(x+y)+z=x+(y+z)$, $x+y=y+x$, $x+0=x$, $xy=yx$, $x\cdot1=x$, $x(y+z)=xy+xz$, and for every $x$ some $w\in R$ with $x+w=0$. Computations with elements of $\mathbb{N}_{0}$ use the laws of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws. For $n\in\mathbb{N}$ the image $n_{R}$ is the finite sum, for the addition of $R$, of the constant map $k\mapsto1$ on $[n]$, by The Image of a Natural Number in a Commutative Ring §image; the constant maps on the various $[n]$ all have the value $1$ of $R$.

Constants. By The Image of a Natural Number in a Commutative Ring §image, $0_{R}=0$. Since $1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $1_{R}=\sum_{k=1}^{1}1$, and the first part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion, applied with $n=1$ to the constant map on $[1]$, gives $1_{R}=1$.

Successor step. We show $(n+1)_{R}=n_{R}+1$ for every $n\in\mathbb{N}_{0}$. If $n=0$, then $n+1=0+1=1$ in $\mathbb{N}_{0}$, and $0+1=1+0=1$ in $R$; so, by the constants clause, $(0+1)_{R}=1_{R}=1=0+1=0_{R}+1$, where the sum $0+1$ in the first term is formed in $\mathbb{N}_{0}$ and the sum $0+1$ in the fourth term in $R$. If $n\neq0$, then $n\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, and $n+1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations. Let $c$ be the constant map $k\mapsto1$ on $[n+1]$. The second part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion, applied to $c$, gives

$$(n+1)_{R}=\sum_{k=1}^{n+1}c_{k}=\Big(\sum_{k=1}^{n}c_{k}\Big)+c_{n+1}=n_{R}+1,$$

because $\sum_{k=1}^{n}c_{k}$ is the finite sum of $c|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §restriction, which applies as $[n]\subseteq[n+1]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, and $c|_{[n]}$ is the constant map $k\mapsto1$ on $[n]$, whose finite sum is $n_{R}$; and $c_{n+1}=1$.

Sum. Fix $m\in\mathbb{N}_{0}$; we prove $(m+n)_{R}=m_{R}+n_{R}$ for every $n\in\mathbb{N}_{0}$ by induction from $0$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction. For $n=0$, $(m+0)_{R}=m_{R}=m_{R}+0=m_{R}+0_{R}$. If the claim holds for $n$, then, using $m+(n+1)=(m+n)+1$, the successor step twice, the induction hypothesis and associativity in $R$,

$$(m+(n+1))_{R}=((m+n)+1)_{R}=(m+n)_{R}+1=(m_{R}+n_{R})+1=m_{R}+(n_{R}+1)=m_{R}+(n+1)_{R}.$$

Zero factor in $R$. For every $x\in R$, $x\cdot0=0$. Indeed $0+0=0$, so $x\cdot0=x(0+0)=x\cdot0+x\cdot0$. Let $w\in R$ with $x\cdot0+w=0$. Then

$$0=x\cdot0+w=(x\cdot0+x\cdot0)+w=x\cdot0+(x\cdot0+w)=x\cdot0+0=x\cdot0.$$

Product. Fix $m\in\mathbb{N}_{0}$; we prove $(mn)_{R}=m_{R}\,n_{R}$ for every $n\in\mathbb{N}_{0}$ by induction from $0$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction. For $n=0$, $m\cdot0=0$ in $\mathbb{N}_{0}$, so $(m\cdot0)_{R}=0_{R}=0=m_{R}\cdot0=m_{R}\,0_{R}$ by the zero factor in $R$. If the claim holds for $n$, then, using $m(n+1)=mn+m\cdot1=mn+m$ in $\mathbb{N}_{0}$, the sum clause, the induction hypothesis, $x\cdot1=x$, distributivity in $R$ and the successor step,

$$(m(n+1))_{R}=(mn+m)_{R}=(mn)_{R}+m_{R}=m_{R}\,n_{R}+m_{R}\cdot1=m_{R}(n_{R}+1)=m_{R}\,(n+1)_{R}.$$