Definition df-zn

Description: Define the ring of integers mod n . This is literally the quotient ring of ZZ by the ideal n ZZ , but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czn	$$class\mathrm{\mathbb{Z}/n\mathbb{Z}}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		zring	$$class{\mathbb{Z}}_{\mathrm{ring}}$$
4		vz	$$setvarz$$
5	4	cv	$$setvarz$$
6		cqus	$$class{/}_{𝑠}$$
7		cqg	$$class{~}_{\mathit{QG}}$$
8		crsp	$$class\mathrm{RSpan}$$
9	5 8	cfv	$$class\mathrm{RSpan}\left(z\right)$$
10	1	cv	$$setvarn$$
11	10	csn	$$class\left\{n\right\}$$
12	11 9	cfv	$$class\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)$$
13	5 12 7	co	$$class\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)$$
14	5 13 6	co	$$class\left(z{/}_{𝑠}\left(z{~}_{\mathit{QG}}\mathrm{RSpan}\left(z\right)\left(\left\{n\right\}\right)\right)\right)$$
15		vs	$$setvars$$
16	15	cv	$$setvars$$
17		csts	$$class\mathrm{sSet}$$
18		cple	$$class\mathrm{le}$$
19		cnx	$$class\mathrm{ndx}$$
20	19 18	cfv	$$class{\le }_{\mathrm{ndx}}$$
21		czrh	$$class\mathrm{\mathbb{Z}RHom}$$
22	16 21	cfv	$$class\mathrm{\mathbb{Z}RHom}\left(s\right)$$
23		cc0	$$class0$$
24	10 23	wceq	$$wffn=0$$
25		cz	$$class\mathbb{Z}$$
26		cfzo	$$class..^$$
27	23 10 26	co	$$class\left(0..^n\right)$$
28	24 25 27	cif	$$classif\left(n=0,\mathbb{Z},\left(0..^n\right)\right)$$
29	22 28	cres	$$class\left({\mathrm{\mathbb{Z}RHom}\left(s\right)\upharpoonright }_{if\left(n=0,\mathbb{Z},\left(0..^n\right)\right)}\right)$$
30		vf	$$setvarf$$
31	30	cv	$$setvarf$$
32		cle	$$class\le$$
33	31 32	ccom	$$class\left(f\circ \le \right)$$
34	31	ccnv	$$class{f}^{-1}$$
35	33 34	ccom	$$class\left(\left(f\circ \le \right)\circ f^{-1}\right)$$
36	30 29 35	csb	$$class⦋\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)$$
37	20 36	cop	$$class⟨{\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)⟩$$
38	16 37 17	co	$$class\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)$$
39	15 14 38	csb	$$class⦋\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)$$
40	4 3 39	csb	$$class⦋{\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)$$
41	1 2 40	cmpt	$$class\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)$$
42	0 41	wceq	$$wff\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)$$