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 21275
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 21271 . 2 class β„€/nβ„€
2 vn . . 3 setvar 𝑛
3 cn0 12476 . . 3 class β„•0
4 vz . . . 4 setvar 𝑧
5 czring 21217 . . . 4 class β„€ring
6 vs . . . . 5 setvar 𝑠
74cv 1540 . . . . . 6 class 𝑧
82cv 1540 . . . . . . . . 9 class 𝑛
98csn 4628 . . . . . . . 8 class {𝑛}
10 crsp 20929 . . . . . . . . 9 class RSpan
117, 10cfv 6543 . . . . . . . 8 class (RSpanβ€˜π‘§)
129, 11cfv 6543 . . . . . . 7 class ((RSpanβ€˜π‘§)β€˜{𝑛})
13 cqg 19038 . . . . . . 7 class ~QG
147, 12, 13co 7411 . . . . . 6 class (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))
15 cqus 17455 . . . . . 6 class /s
167, 14, 15co 7411 . . . . 5 class (𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛})))
176cv 1540 . . . . . 6 class 𝑠
18 cnx 17130 . . . . . . . 8 class ndx
19 cple 17208 . . . . . . . 8 class le
2018, 19cfv 6543 . . . . . . 7 class (leβ€˜ndx)
21 vf . . . . . . . 8 setvar 𝑓
22 czrh 21268 . . . . . . . . . 10 class β„€RHom
2317, 22cfv 6543 . . . . . . . . 9 class (β„€RHomβ€˜π‘ )
24 cc0 11112 . . . . . . . . . . 11 class 0
258, 24wceq 1541 . . . . . . . . . 10 wff 𝑛 = 0
26 cz 12562 . . . . . . . . . 10 class β„€
27 cfzo 13631 . . . . . . . . . . 11 class ..^
2824, 8, 27co 7411 . . . . . . . . . 10 class (0..^𝑛)
2925, 26, 28cif 4528 . . . . . . . . 9 class if(𝑛 = 0, β„€, (0..^𝑛))
3023, 29cres 5678 . . . . . . . 8 class ((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛)))
3121cv 1540 . . . . . . . . . 10 class 𝑓
32 cle 11253 . . . . . . . . . 10 class ≀
3331, 32ccom 5680 . . . . . . . . 9 class (𝑓 ∘ ≀ )
3431ccnv 5675 . . . . . . . . 9 class ◑𝑓
3533, 34ccom 5680 . . . . . . . 8 class ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3621, 30, 35csb 3893 . . . . . . 7 class ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)
3720, 36cop 4634 . . . . . 6 class ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩
38 csts 17100 . . . . . 6 class sSet
3917, 37, 38co 7411 . . . . 5 class (𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
406, 16, 39csb 3893 . . . 4 class ⦋(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
414, 5, 40csb 3893 . . 3 class ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩)
422, 3, 41cmpt 5231 . 2 class (𝑛 ∈ β„•0 ↦ ⦋℀ring / π‘§β¦Œβ¦‹(𝑧 /s (𝑧 ~QG ((RSpanβ€˜π‘§)β€˜{𝑛}))) / π‘ β¦Œ(𝑠 sSet ⟨(leβ€˜ndx), ⦋((β„€RHomβ€˜π‘ ) β†Ύ if(𝑛 = 0, β„€, (0..^𝑛))) / π‘“β¦Œ((𝑓 ∘ ≀ ) ∘ ◑𝑓)⟩))
431, 42wceq 1541 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  21306
  Copyright terms: Public domain W3C validator