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

Definition df-zn 19774
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 19770 . 2 class ℤ/n
2 vn . . 3 setvar 𝑛
3 cn0 11236 . . 3 class 0
4 vz . . . 4 setvar 𝑧
5 zring 19737 . . . 4 class ring
6 vs . . . . 5 setvar 𝑠
74cv 1479 . . . . . 6 class 𝑧
82cv 1479 . . . . . . . . 9 class 𝑛
98csn 4148 . . . . . . . 8 class {𝑛}
10 crsp 19090 . . . . . . . . 9 class RSpan
117, 10cfv 5847 . . . . . . . 8 class (RSpan‘𝑧)
129, 11cfv 5847 . . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13 cqg 17511 . . . . . . 7 class ~QG
147, 12, 13co 6604 . . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15 cqus 16086 . . . . . 6 class /s
167, 14, 15co 6604 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
176cv 1479 . . . . . 6 class 𝑠
18 cnx 15778 . . . . . . . 8 class ndx
19 cple 15869 . . . . . . . 8 class le
2018, 19cfv 5847 . . . . . . 7 class (le‘ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 19767 . . . . . . . . . 10 class ℤRHom
2317, 22cfv 5847 . . . . . . . . 9 class (ℤRHom‘𝑠)
24 cc0 9880 . . . . . . . . . . 11 class 0
258, 24wceq 1480 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 11321 . . . . . . . . . 10 class
27 cfzo 12406 . . . . . . . . . . 11 class ..^
2824, 8, 27co 6604 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4058 . . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
3023, 29cres 5076 . . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
3121cv 1479 . . . . . . . . . 10 class 𝑓
32 cle 10019 . . . . . . . . . 10 class
3331, 32ccom 5078 . . . . . . . . 9 class (𝑓 ∘ ≤ )
3431ccnv 5073 . . . . . . . . 9 class 𝑓
3533, 34ccom 5078 . . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ 𝑓)
3621, 30, 35csb 3514 . . . . . . 7 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)
3720, 36cop 4154 . . . . . 6 class ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩
38 csts 15779 . . . . . 6 class sSet
3917, 37, 38co 6604 . . . . 5 class (𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
406, 16, 39csb 3514 . . . 4 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
414, 5, 40csb 3514 . . 3 class ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
422, 3, 41cmpt 4673 . 2 class (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
431, 42wceq 1480 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  19802
  Copyright terms: Public domain W3C validator