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 21056
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 21052 . 2 class β„€/nβ„€
2 vn . . 3 setvar 𝑛
3 cn0 12472 . . 3 class β„•0
4 vz . . . 4 setvar 𝑧
5 czring 21017 . . . 4 class β„€ring
6 vs . . . . 5 setvar 𝑠
74cv 1541 . . . . . 6 class 𝑧
82cv 1541 . . . . . . . . 9 class 𝑛
98csn 4629 . . . . . . . 8 class {𝑛}
10 crsp 20784 . . . . . . . . 9 class RSpan
117, 10cfv 6544 . . . . . . . 8 class (RSpanβ€˜π‘§)
129, 11cfv 6544 . . . . . . 7 class ((RSpanβ€˜π‘§)β€˜{𝑛})
13 cqg 19002 . . . . . . 7 class ~QG
147, 12, 13co 7409 . . . . . 6 class (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))
15 cqus 17451 . . . . . 6 class /s
167, 14, 15co 7409 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛})))
176cv 1541 . . . . . 6 class 𝑠
18 cnx 17126 . . . . . . . 8 class ndx
19 cple 17204 . . . . . . . 8 class le
2018, 19cfv 6544 . . . . . . 7 class (leβ€˜ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 21049 . . . . . . . . . 10 class β„€RHom
2317, 22cfv 6544 . . . . . . . . 9 class (β„€RHomβ€˜π‘ )
24 cc0 11110 . . . . . . . . . . 11 class 0
258, 24wceq 1542 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 12558 . . . . . . . . . 10 class β„€
27 cfzo 13627 . . . . . . . . . . 11 class ..^
2824, 8, 27co 7409 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4529 . . . . . . . . 9 class if(𝑛 = 0, β„€, (0..^𝑛))
3023, 29cres 5679 . . . . . . . 8 class ((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛)))
3121cv 1541 . . . . . . . . . 10 class 𝑓
32 cle 11249 . . . . . . . . . 10 class ≀
3331, 32ccom 5681 . . . . . . . . 9 class (𝑓 ∘ ≀ )
3431ccnv 5676 . . . . . . . . 9 class ◑𝑓
3533, 34ccom 5681 . . . . . . . 8 class ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3621, 30, 35csb 3894 . . . . . . 7 class ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3720, 36cop 4635 . . . . . 6 class ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩
38 csts 17096 . . . . . 6 class sSet
3917, 37, 38co 7409 . . . . 5 class (𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
406, 16, 39csb 3894 . . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
414, 5, 40csb 3894 . . 3 class ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
422, 3, 41cmpt 5232 . 2 class (𝑛 ∈ β„•0 ↦ ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩))
431, 42wceq 1542 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  21087
  Copyright terms: Public domain W3C validator