Proof of Elementwise Laws of a Commutative Ring

The ring data. By Commutative Rings §ring, $R$ is a set, $+$ and $\cdot$ are binary operations on $R$, written as in Binary Operations on a Set §notation, $0\in R$ and $1\in R$, and the laws listed there hold for all elements of $R$. Below, those laws are used instantiated at elements of $R$.

Clause closure. Since $+$ is a binary operation on the set $R$ and $x,y\in R$, Binary Operations on a Set §notation gives that the value $x+y$ exists and lies in $R$; likewise, since $\cdot$ is a binary operation on $R$, $x\cdot y\in R$. Finally $0\in R$ and $1\in R$ by Commutative Rings §ring.

Clauses add-associative and add-commutative. These are the associative and commutative laws for $+$ of Commutative Rings §ring at $x$, $y$, $z$.

Clause add-zero. $x+0=x$ is the law $x+0=x$ of Commutative Rings §ring at $x$. Since $0\in R$ by the clause closure, the commutative law for $+$ at $0$ and $x$ gives $0+x=x+0$, and $x+0=x$; so $0+x=x$.

Clauses mul-associative and mul-commutative. These are the associative and commutative laws for $\cdot$ of Commutative Rings §ring at $x$, $y$, $z$.

Clause mul-one. $x\cdot1=x$ is the law $x\cdot1=x$ of Commutative Rings §ring at $x$. Since $1\in R$ by the clause closure, the commutative law for $\cdot$ at $1$ and $x$ gives $1\cdot x=x\cdot1$, and $x\cdot1=x$; so $1\cdot x=x$.

Clause distributive. The first equation is the distributive law of Commutative Rings §ring at $x$, $y$, $z$. For the second, $x+y\in R$ by the clause closure, so the commutative law for $\cdot$ at $x+y$ and $z$ gives $(x+y)\cdot z=z\cdot(x+y)$; the distributive law at $z$, $x$, $y$ gives $z\cdot(x+y)=z\cdot x+z\cdot y$; and the commutative law for $\cdot$ gives $z\cdot x=x\cdot z$ and $z\cdot y=y\cdot z$, so $z\cdot x+z\cdot y=x\cdot z+y\cdot z$. Together, $(x+y)\cdot z=x\cdot z+y\cdot z$.