Theorem znbas2

Description: The base set 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	znbas2	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_U={\mathrm{Base}}_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		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
6	5	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
7	1 2 3 4 6	znbaslem	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_U={\mathrm{Base}}_Y$$