Theorem znbas

Description: The base set of Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znbas.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znbas.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znbas.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)$$
Assertion	znbas	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/R={\mathrm{Base}}_Y$$

Proof

Step	Hyp	Ref	Expression
1		znbas.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znbas.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
3		znbas.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)$$
4		eqidd	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}R={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}R$$
5		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7	3	ovexi	$$⊢R\in \mathrm{V}$$
8	7	a1i	$$⊢N\in {\mathbb{N}}_0\to R\in \mathrm{V}$$
9		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
10	9	a1i	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
11	4 6 8 10	qusbas	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/R={\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}R\right)}$$
12	3	oveq2i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}R={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
13	1 12 2	znbas2	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}R\right)}={\mathrm{Base}}_Y$$
14	11 13	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/R={\mathrm{Base}}_Y$$