Theorem znbaslem

Description: Lemma for znbas . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by AV, 13-Jun-2019) (Revised by AV, 9-Sep-2021) (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}$$
	znbaslem.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	znbaslem.n	$$⊢E\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
Assertion	znbaslem	$$⊢N\in {\mathbb{N}}_0\to E\left(U\right)=E\left(Y\right)$$

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		znbaslem.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
5		znbaslem.n	$$⊢E\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
6	4 5	setsnid	$$⊢E\left(U\right)=E\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩\right)$$
7		eqid	$$⊢{\le }_Y={\le }_Y$$
8	1 2 3 7	znval2	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩$$
9	8	fveq2d	$$⊢N\in {\mathbb{N}}_0\to E\left(Y\right)=E\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩\right)$$
10	6 9	eqtr4id	$$⊢N\in {\mathbb{N}}_0\to E\left(U\right)=E\left(Y\right)$$