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 20070
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 20066 . 2 class ℤ/n
2 vn . . 3 setvar 𝑛
3 cn0 11499 . . 3 class 0
4 vz . . . 4 setvar 𝑧
5 zring 20033 . . . 4 class ring
6 vs . . . . 5 setvar 𝑠
74cv 1630 . . . . . 6 class 𝑧
82cv 1630 . . . . . . . . 9 class 𝑛
98csn 4317 . . . . . . . 8 class {𝑛}
10 crsp 19386 . . . . . . . . 9 class RSpan
117, 10cfv 6030 . . . . . . . 8 class (RSpan‘𝑧)
129, 11cfv 6030 . . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13 cqg 17798 . . . . . . 7 class ~QG
147, 12, 13co 6796 . . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15 cqus 16373 . . . . . 6 class /s
167, 14, 15co 6796 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
176cv 1630 . . . . . 6 class 𝑠
18 cnx 16061 . . . . . . . 8 class ndx
19 cple 16156 . . . . . . . 8 class le
2018, 19cfv 6030 . . . . . . 7 class (le‘ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 20063 . . . . . . . . . 10 class ℤRHom
2317, 22cfv 6030 . . . . . . . . 9 class (ℤRHom‘𝑠)
24 cc0 10142 . . . . . . . . . . 11 class 0
258, 24wceq 1631 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 11584 . . . . . . . . . 10 class
27 cfzo 12673 . . . . . . . . . . 11 class ..^
2824, 8, 27co 6796 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4226 . . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
3023, 29cres 5252 . . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
3121cv 1630 . . . . . . . . . 10 class 𝑓
32 cle 10281 . . . . . . . . . 10 class
3331, 32ccom 5254 . . . . . . . . 9 class (𝑓 ∘ ≤ )
3431ccnv 5249 . . . . . . . . 9 class 𝑓
3533, 34ccom 5254 . . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ 𝑓)
3621, 30, 35csb 3682 . . . . . . 7 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)
3720, 36cop 4323 . . . . . 6 class ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩
38 csts 16062 . . . . . 6 class sSet
3917, 37, 38co 6796 . . . . 5 class (𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
406, 16, 39csb 3682 . . . 4 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
414, 5, 40csb 3682 . . 3 class ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
422, 3, 41cmpt 4864 . 2 class (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
431, 42wceq 1631 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  20098
  Copyright terms: Public domain W3C validator