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)

	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}K$$
	znbaslem.k	$$⊢K\in \mathbb{N}$$
	znbaslem.l	$$⊢K<10$$
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}K$$
5		znbaslem.k	$$⊢K\in \mathbb{N}$$
6		znbaslem.l	$$⊢K<10$$
7	4 5	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
8	5	nnrei	$$⊢K\in ℝ$$
9	8 6	ltneii	$$⊢K\ne 10$$
10	4 5	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=K$$
11		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
12	10 11	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\leftrightarrow K\ne 10$$
13	9 12	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
14	7 13	setsnid	$$⊢E\left(U\right)=E\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩\right)$$
15		eqid	$$⊢{\le }_Y={\le }_Y$$
16	1 2 3 15	znval2	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩$$
17	16	fveq2d	$$⊢N\in {\mathbb{N}}_0\to E\left(Y\right)=E\left(U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\le }_Y⟩\right)$$
18	14 17	eqtr4id	$$⊢N\in {\mathbb{N}}_0\to E\left(U\right)=E\left(Y\right)$$