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 20055
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 20051 . 2 class ℤ/n
2 vn . . 3 setvar 𝑛
3 cn0 11482 . . 3 class 0
4 vz . . . 4 setvar 𝑧
5 zring 20018 . . . 4 class ring
6 vs . . . . 5 setvar 𝑠
74cv 1629 . . . . . 6 class 𝑧
82cv 1629 . . . . . . . . 9 class 𝑛
98csn 4319 . . . . . . . 8 class {𝑛}
10 crsp 19371 . . . . . . . . 9 class RSpan
117, 10cfv 6047 . . . . . . . 8 class (RSpan‘𝑧)
129, 11cfv 6047 . . . . . . 7 class ((RSpan‘𝑧)‘{𝑛})
13 cqg 17789 . . . . . . 7 class ~QG
147, 12, 13co 6811 . . . . . 6 class (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))
15 cqus 16365 . . . . . 6 class /s
167, 14, 15co 6811 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))
176cv 1629 . . . . . 6 class 𝑠
18 cnx 16054 . . . . . . . 8 class ndx
19 cple 16148 . . . . . . . 8 class le
2018, 19cfv 6047 . . . . . . 7 class (le‘ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 20048 . . . . . . . . . 10 class ℤRHom
2317, 22cfv 6047 . . . . . . . . 9 class (ℤRHom‘𝑠)
24 cc0 10126 . . . . . . . . . . 11 class 0
258, 24wceq 1630 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 11567 . . . . . . . . . 10 class
27 cfzo 12657 . . . . . . . . . . 11 class ..^
2824, 8, 27co 6811 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4228 . . . . . . . . 9 class if(𝑛 = 0, ℤ, (0..^𝑛))
3023, 29cres 5266 . . . . . . . 8 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))
3121cv 1629 . . . . . . . . . 10 class 𝑓
32 cle 10265 . . . . . . . . . 10 class
3331, 32ccom 5268 . . . . . . . . 9 class (𝑓 ∘ ≤ )
3431ccnv 5263 . . . . . . . . 9 class 𝑓
3533, 34ccom 5268 . . . . . . . 8 class ((𝑓 ∘ ≤ ) ∘ 𝑓)
3621, 30, 35csb 3672 . . . . . . 7 class ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)
3720, 36cop 4325 . . . . . 6 class ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩
38 csts 16055 . . . . . 6 class sSet
3917, 37, 38co 6811 . . . . 5 class (𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
406, 16, 39csb 3672 . . . 4 class (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
414, 5, 40csb 3672 . . 3 class ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩)
422, 3, 41cmpt 4879 . 2 class (𝑛 ∈ ℕ0ring / 𝑧(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠(𝑠 sSet ⟨(le‘ndx), ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓((𝑓 ∘ ≤ ) ∘ 𝑓)⟩))
431, 42wceq 1630 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  20083
  Copyright terms: Public domain W3C validator