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)

	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		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		1lt10	$$⊢1<10$$
7	1 2 3 4 5 6	znbaslem	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_U={\mathrm{Base}}_Y$$