Definition df-zn 19855

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 19851	. 2 class ℤ/nℤ
2		vn	. . 3 setvar 𝑛
3		cn0 11292	. . 3 class ℕ0
4		vz	. . . 4 setvar 𝑧
5		zring 19818	. . . 4 class ℤring
6		vs	. . . . 5 setvar 𝑠
7	4	cv 1482	. . . . . 6 class 𝑧
8	2	cv 1482	. . . . . . . . 9 class 𝑛
9	8	csn 4177	. . . . . . . 8 class {𝑛}
10		crsp 19171	. . . . . . . . 9 class RSpan
11	7, 10	cfv 5888	. . . . . . . 8 class (RSpan‘𝑧)
12	9, 11	cfv 5888	. . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13		cqg 17590	. . . . . . 7 class ~QG
14	7, 12, 13	co 6650	. . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15		cqus 16165	. . . . . 6 class /s
16	7, 14, 15	co 6650	. . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
17	6	cv 1482	. . . . . 6 class 𝑠
18		cnx 15854	. . . . . . . 8 class ndx
19		cple 15948	. . . . . . . 8 class le
20	18, 19	cfv 5888	. . . . . . 7 class (le‘ndx)
21		vf	. . . . . . . 8 setvar 𝑓
22		czrh 19848	. . . . . . . . . 10 class ℤRHom
23	17, 22	cfv 5888	. . . . . . . . 9 class (ℤRHom‘𝑠)
24		cc0 9936	. . . . . . . . . . 11 class 0
25	8, 24	wceq 1483	. . . . . . . . . 10 wff 𝑛 = 0
26		cz 11377	. . . . . . . . . 10 class ℤ
27		cfzo 12465	. . . . . . . . . . 11 class ..^
28	24, 8, 27	co 6650	. . . . . . . . . 10 class (0..^𝑛)
29	25, 26, 28	cif 4086	. . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
30	23, 29	cres 5116	. . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
31	21	cv 1482	. . . . . . . . . 10 class 𝑓
32		cle 10075	. . . . . . . . . 10 class ≤
33	31, 32	ccom 5118	. . . . . . . . 9 class (𝑓 ∘ ≤ )
34	31	ccnv 5113	. . . . . . . . 9 class ◡𝑓
35	33, 34	ccom 5118	. . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ ◡𝑓)
36	21, 30, 35	csb 3533	. . . . . . 7 class ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)
37	20, 36	cop 4183	. . . . . 6 class ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩
38		csts 15855	. . . . . 6 class sSet
39	17, 37, 38	co 6650	. . . . 5 class (𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
40	6, 16, 39	csb 3533	. . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
41	4, 5, 40	csb 3533	. . 3 class ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩)
42	2, 3, 41	cmpt 4729	. 2 class (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
43	1, 42	wceq 1483	1 wff ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))

This definition is referenced by:  znval  19883