Definition df-zn 20753

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 20749	. 2 class ℤ/nℤ
2		vn	. . 3 setvar 𝑛
3		cn0 12279	. . 3 class ℕ0
4		vz	. . . 4 setvar 𝑧
5		czring 20715	. . . 4 class ℤring
6		vs	. . . . 5 setvar 𝑠
7	4	cv 1538	. . . . . 6 class 𝑧
8	2	cv 1538	. . . . . . . . 9 class 𝑛
9	8	csn 4565	. . . . . . . 8 class {𝑛}
10		crsp 20478	. . . . . . . . 9 class RSpan
11	7, 10	cfv 6458	. . . . . . . 8 class (RSpan‘𝑧)
12	9, 11	cfv 6458	. . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13		cqg 18796	. . . . . . 7 class ~QG
14	7, 12, 13	co 7307	. . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15		cqus 17261	. . . . . 6 class /s
16	7, 14, 15	co 7307	. . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
17	6	cv 1538	. . . . . 6 class 𝑠
18		cnx 16939	. . . . . . . 8 class ndx
19		cple 17014	. . . . . . . 8 class le
20	18, 19	cfv 6458	. . . . . . 7 class (le‘ndx)
21		vf	. . . . . . . 8 setvar 𝑓
22		czrh 20746	. . . . . . . . . 10 class ℤRHom
23	17, 22	cfv 6458	. . . . . . . . 9 class (ℤRHom‘𝑠)
24		cc0 10917	. . . . . . . . . . 11 class 0
25	8, 24	wceq 1539	. . . . . . . . . 10 wff 𝑛 = 0
26		cz 12365	. . . . . . . . . 10 class ℤ
27		cfzo 13428	. . . . . . . . . . 11 class ..^
28	24, 8, 27	co 7307	. . . . . . . . . 10 class (0..^𝑛)
29	25, 26, 28	cif 4465	. . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
30	23, 29	cres 5602	. . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
31	21	cv 1538	. . . . . . . . . 10 class 𝑓
32		cle 11056	. . . . . . . . . 10 class ≤
33	31, 32	ccom 5604	. . . . . . . . 9 class (𝑓 ∘ ≤ )
34	31	ccnv 5599	. . . . . . . . 9 class ◡𝑓
35	33, 34	ccom 5604	. . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ ◡𝑓)
36	21, 30, 35	csb 3837	. . . . . . 7 class ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)
37	20, 36	cop 4571	. . . . . 6 class ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩
38		csts 16909	. . . . . 6 class sSet
39	17, 37, 38	co 7307	. . . . 5 class (𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
40	6, 16, 39	csb 3837	. . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
41	4, 5, 40	csb 3837	. . 3 class ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
42	2, 3, 41	cmpt 5164	. 2 class (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
43	1, 42	wceq 1539	1 wff ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))

This definition is referenced by:  znval  20784