Theorem znmul

Description: The multiplicative 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	znmul	$$⊢N\in {\mathbb{N}}_0\to {\cdot }_U={\cdot }_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		mulrid	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
5		plendxnmulrndx	$$⊢{\le }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
6	5	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
7	1 2 3 4 6	znbaslem	$$⊢N\in {\mathbb{N}}_0\to {\cdot }_U={\cdot }_Y$$