Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-zn Structured version   Visualization version   GIF version

Definition df-zn 20205
 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ℤ = (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
Distinct variable group:   𝑧,𝑛,𝑠,𝑓

Detailed syntax breakdown of Definition df-zn
StepHypRef Expression
1 czn 20201 . 2 class ℤ/n
2 vn . . 3 setvar 𝑛
3 cn0 11888 . . 3 class 0
4 vz . . . 4 setvar 𝑧
5 zring 20167 . . . 4 class ring
6 vs . . . . 5 setvar 𝑠
74cv 1537 . . . . . 6 class 𝑧
82cv 1537 . . . . . . . . 9 class 𝑛
98csn 4525 . . . . . . . 8 class {𝑛}
10 crsp 19940 . . . . . . . . 9 class RSpan
117, 10cfv 6325 . . . . . . . 8 class (RSpan‘𝑧)
129, 11cfv 6325 . . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13 cqg 18271 . . . . . . 7 class ~QG
147, 12, 13co 7136 . . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15 cqus 16773 . . . . . 6 class /s
167, 14, 15co 7136 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
176cv 1537 . . . . . 6 class 𝑠
18 cnx 16475 . . . . . . . 8 class ndx
19 cple 16567 . . . . . . . 8 class le
2018, 19cfv 6325 . . . . . . 7 class (le‘ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 20198 . . . . . . . . . 10 class ℤRHom
2317, 22cfv 6325 . . . . . . . . 9 class (ℤRHom‘𝑠)
24 cc0 10529 . . . . . . . . . . 11 class 0
258, 24wceq 1538 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 11972 . . . . . . . . . 10 class
27 cfzo 13031 . . . . . . . . . . 11 class ..^
2824, 8, 27co 7136 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4425 . . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
3023, 29cres 5522 . . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
3121cv 1537 . . . . . . . . . 10 class 𝑓
32 cle 10668 . . . . . . . . . 10 class
3331, 32ccom 5524 . . . . . . . . 9 class (𝑓 ∘ ≤ )
3431ccnv 5519 . . . . . . . . 9 class 𝑓
3533, 34ccom 5524 . . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ 𝑓)
3621, 30, 35csb 3828 . . . . . . 7 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)
3720, 36cop 4531 . . . . . 6 class ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩
38 csts 16476 . . . . . 6 class sSet
3917, 37, 38co 7136 . . . . 5 class (𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
406, 16, 39csb 3828 . . . 4 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
414, 5, 40csb 3828 . . 3 class ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
422, 3, 41cmpt 5111 . 2 class (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
431, 42wceq 1538 1 wff ℤ/nℤ = (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
 Colors of variables: wff setvar class This definition is referenced by:  znval  20232
 Copyright terms: Public domain W3C validator