Theorem znval

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 2-May-2016) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
	znval.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znval.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W$$
	znval.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
	znval.l	$$⊢\underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$
Assertion	znval	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$

Proof

Step	Hyp	Ref	Expression
1		znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		znval.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		znval.f	$$⊢F={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W$$
5		znval.w	$$⊢W=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
6		znval.l	$$⊢\underset{\dot{}}{\le }=\left(F\circ \le \right)\circ F^{-1}$$
7		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
8	7	a1i	$$⊢n=N\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
9		ovexd	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\in \mathrm{V}$$
10		id	$$⊢s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\to s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)$$
11		simpr	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to z={\mathbb{Z}}_{\mathrm{ring}}$$
12	11	fveq2d	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to \mathrm{RSpan}\left(z\right)=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
13	12 1	eqtr4di	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to \mathrm{RSpan}\left(z\right)=S$$
14		simpl	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to n=N$$
15	14	sneqd	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to \left\{n\right\}=\left\{N\right\}$$
16	13 15	fveq12d	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to \mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)=S\left(\left\{N\right\}\right)$$
17	11 16	oveq12d	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)$$
18	11 17	oveq12d	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
19	18 2	eqtr4di	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)=U$$
20	10 19	sylan9eqr	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to s=U$$
21		fvex	$$⊢\mathrm{\mathbb{Z}RHom}\left(s\right)\in \mathrm{V}$$
22	21	resex	$$⊢{\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\in \mathrm{V}$$
23	22	a1i	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to {\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\in \mathrm{V}$$
24		id	$$⊢f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\to f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}$$
25	20	fveq2d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(s\right)=\mathrm{\mathbb{Z}RHom}\left(U\right)$$
26		simpll	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to n=N$$
27	26	eqeq1d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to \left(n=0\leftrightarrow N=0\right)$$
28	26	oveq2d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to \left(0..^n\right)=\left(0..^N\right)$$
29	27 28	ifbieq2d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
30	29 5	eqtr4di	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)=W$$
31	25 30	reseq12d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to {\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}={\mathrm{\mathbb{Z}RHom}\left(U\right)\upharpoonright }_W$$
32	31 4	eqtr4di	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to {\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}=F$$
33	24 32	sylan9eqr	$$⊢\left(\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\wedge f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)\to f=F$$
34	33	coeq1d	$$⊢\left(\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\wedge f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)\to f\circ \le =F\circ \le$$
35	33	cnveqd	$$⊢\left(\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\wedge f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)\to f^{-1}=F^{-1}$$
36	34 35	coeq12d	$$⊢\left(\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\wedge f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)\to \left(f\circ \le \right)\circ f^{-1}=\left(F\circ \le \right)\circ F^{-1}$$
37	36 6	eqtr4di	$$⊢\left(\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\wedge f={\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)\to \left(f\circ \le \right)\circ f^{-1}=\underset{\dot{}}{\le }$$
38	23 37	csbied	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to ⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)=\underset{\dot{}}{\le }$$
39	38	opeq2d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to ⟨{\le }_{\mathrm{ndx}},⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)⟩=⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
40	20 39	oveq12d	$$⊢\left(\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\wedge s=z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)\to s\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)⟩=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
41	9 40	csbied	$$⊢\left(n=N\wedge z={\mathbb{Z}}_{\mathrm{ring}}\right)\to ⦋\left(z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)/s⦌\left(s\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)⟩\right)=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
42	8 41	csbied	$$⊢n=N\to ⦋{\mathbb{Z}}_{\mathrm{ring}}/z⦌⦋\left(z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)/s⦌\left(s\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)⟩\right)=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
43		df-zn	$$⊢\mathrm{\mathbb{Z}/n\mathbb{Z}}=\left(n\in {\mathbb{N}}_0⟼⦋{\mathbb{Z}}_{\mathrm{ring}}/z⦌⦋\left(z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)/s⦌\left(s\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},⦋\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)/f⦌\left(\left(f\circ \le \right)\circ f^{-1}\right)⟩\right)\right)$$
44		ovex	$$⊢U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\in \mathrm{V}$$
45	42 43 44	fvmpt	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/N\mathbb{Z}=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
46	3 45	eqtrid	$$⊢N\in {\mathbb{N}}_0\to Y=U\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$