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 21560
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
StepHypRef Expression
1 czn 21556 . 2 class β„€/nβ„€
2 vn . . 3 setvar 𝑛
3 cn0 12558 . . 3 class β„•0
4 vz . . . 4 setvar 𝑧
5 czring 21500 . . . 4 class β„€ring
6 vs . . . . 5 setvar 𝑠
74cv 1536 . . . . . 6 class 𝑧
82cv 1536 . . . . . . . . 9 class 𝑛
98csn 4648 . . . . . . . 8 class {𝑛}
10 crsp 21260 . . . . . . . . 9 class RSpan
117, 10cfv 6576 . . . . . . . 8 class (RSpanβ€˜π‘§)
129, 11cfv 6576 . . . . . . 7 class ((RSpanβ€˜π‘§)β€˜{𝑛})
13 cqg 19182 . . . . . . 7 class ~QG
147, 12, 13co 7451 . . . . . 6 class (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))
15 cqus 17585 . . . . . 6 class /s
167, 14, 15co 7451 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛})))
176cv 1536 . . . . . 6 class 𝑠
18 cnx 17260 . . . . . . . 8 class ndx
19 cple 17338 . . . . . . . 8 class le
2018, 19cfv 6576 . . . . . . 7 class (leβ€˜ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 21553 . . . . . . . . . 10 class β„€RHom
2317, 22cfv 6576 . . . . . . . . 9 class (β„€RHomβ€˜π‘ )
24 cc0 11187 . . . . . . . . . . 11 class 0
258, 24wceq 1537 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 12645 . . . . . . . . . 10 class β„€
27 cfzo 13722 . . . . . . . . . . 11 class ..^
2824, 8, 27co 7451 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4548 . . . . . . . . 9 class if(𝑛 = 0, β„€, (0..^𝑛))
3023, 29cres 5703 . . . . . . . 8 class ((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛)))
3121cv 1536 . . . . . . . . . 10 class 𝑓
32 cle 11328 . . . . . . . . . 10 class ≀
3331, 32ccom 5705 . . . . . . . . 9 class (𝑓 ∘ ≀ )
3431ccnv 5700 . . . . . . . . 9 class ◑𝑓
3533, 34ccom 5705 . . . . . . . 8 class ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3621, 30, 35csb 3921 . . . . . . 7 class ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3720, 36cop 4654 . . . . . 6 class ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩
38 csts 17230 . . . . . 6 class sSet
3917, 37, 38co 7451 . . . . 5 class (𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
406, 16, 39csb 3921 . . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
414, 5, 40csb 3921 . . 3 class ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
422, 3, 41cmpt 5250 . 2 class (𝑛 ∈ β„•0 ↦ ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩))
431, 42wceq 1537 1 wff β„€/nβ„€ = (𝑛 ∈ β„•0 ↦ ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  znval  21593
  Copyright terms: Public domain W3C validator