Definition df-zn 14620

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

Assertion

Ref	Expression
df-zn	⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))

Distinct variable group:   𝑧,𝑛,𝑠,𝑓

Detailed syntax breakdown of Definition df-zn

Step	Hyp	Ref	Expression
1		czn 14617	. 2 class ℤ/nℤ
2		vn	. . 3 setvar 𝑛
3		cn0 9392	. . 3 class ℕ0
4		vz	. . . 4 setvar 𝑧
5		czring 14594	. . . 4 class ℤring
6		vs	. . . . 5 setvar 𝑠
7	4	cv 1394	. . . . . 6 class 𝑧
8	2	cv 1394	. . . . . . . . 9 class 𝑛
9	8	csn 3667	. . . . . . . 8 class {𝑛}
10		crsp 14472	. . . . . . . . 9 class RSpan
11	7, 10	cfv 5324	. . . . . . . 8 class (RSpan‘𝑧)
12	9, 11	cfv 5324	. . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13		cqg 13746	. . . . . . 7 class ~QG
14	7, 12, 13	co 6013	. . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15		cqus 13373	. . . . . 6 class /s
16	7, 14, 15	co 6013	. . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
17	6	cv 1394	. . . . . 6 class 𝑠
18		cnx 13069	. . . . . . . 8 class ndx
19		cple 13157	. . . . . . . 8 class le
20	18, 19	cfv 5324	. . . . . . 7 class (le‘ndx)
21		vf	. . . . . . . 8 setvar 𝑓
22		czrh 14615	. . . . . . . . . 10 class ℤRHom
23	17, 22	cfv 5324	. . . . . . . . 9 class (ℤRHom‘𝑠)
24		cc0 8022	. . . . . . . . . . 11 class 0
25	8, 24	wceq 1395	. . . . . . . . . 10 wff 𝑛 = 0
26		cz 9469	. . . . . . . . . 10 class ℤ
27		cfzo 10367	. . . . . . . . . . 11 class ..^
28	24, 8, 27	co 6013	. . . . . . . . . 10 class (0..^𝑛)
29	25, 26, 28	cif 3603	. . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
30	23, 29	cres 4725	. . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
31	21	cv 1394	. . . . . . . . . 10 class 𝑓
32		cle 8205	. . . . . . . . . 10 class ≤
33	31, 32	ccom 4727	. . . . . . . . 9 class (𝑓 ∘ ≤ )
34	31	ccnv 4722	. . . . . . . . 9 class ◡𝑓
35	33, 34	ccom 4727	. . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ ◡𝑓)
36	21, 30, 35	csb 3125	. . . . . . 7 class ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)
37	20, 36	cop 3670	. . . . . 6 class ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩
38		csts 13070	. . . . . 6 class sSet
39	17, 37, 38	co 6013	. . . . 5 class (𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
40	6, 16, 39	csb 3125	. . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
41	4, 5, 40	csb 3125	. . 3 class ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
42	2, 3, 41	cmpt 4148	. 2 class (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
43	1, 42	wceq 1395	1 wff ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))

This definition is referenced by:  znval  14640