Theorem zncrng

Description: Z/nZ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypothesis	zncrng.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
Assertion	zncrng	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		zncrng.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
3		eqid	$$⊢\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
4		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)$$
5	3 4	zncrng2	$$⊢N\in \mathbb{Z}\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\in \mathrm{CRing}$$
6	2 5	syl	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\in \mathrm{CRing}$$
7		eqidd	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}={\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}$$
8	3 4 1	znbas2	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}={\mathrm{Base}}_Y$$
9	3 4 1	znadd	$$⊢N\in {\mathbb{N}}_0\to {+}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}={+}_Y$$
10	9	oveqdr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}\wedge y\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}\right)\right)\to x{+}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}y=x{+}_{Y}y$$
11	3 4 1	znmul	$$⊢N\in {\mathbb{N}}_0\to {\cdot }_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}={\cdot }_Y$$
12	11	oveqdr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}\wedge y\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}\right)\right)\to x{\cdot }_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)}y=x{\cdot }_{Y}y$$
13	7 8 10 12	crngpropd	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\in \mathrm{CRing}\leftrightarrow Y\in \mathrm{CRing}\right)$$
14	6 13	mpbid	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$