Theorem znadd

Description: The additive structure of Z/nZ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019) (Revised by AV, 3-Nov-2024)

	Ref	Expression
Hypotheses	znval2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
	znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
Assertion	znadd	$$⊢N\in {\mathbb{N}}_0\to {+}_U={+}_Y$$

Proof

Step	Hyp	Ref	Expression
1		znval2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
5		plendxnplusgndx	$$⊢{\le }_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
6	5	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
7	1 2 3 4 6	znbaslem	$$⊢N\in {\mathbb{N}}_0\to {+}_U={+}_Y$$