MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dchr Structured version   Visualization version   GIF version

Definition df-dchr 24675
Description: The group of Dirichlet characters mod 𝑛 is the set of monoid homomorphisms from ℤ / 𝑛 to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.)
Assertion
Ref Expression
df-dchr DChr = (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})
Distinct variable groups:   𝑥,𝑧   𝑛,𝑏,𝑧,𝑥

Detailed syntax breakdown of Definition df-dchr
StepHypRef Expression
1 cdchr 24674 . 2 class DChr
2 vn . . 3 setvar 𝑛
3 cn 10867 . . 3 class
4 vz . . . 4 setvar 𝑧
52cv 1473 . . . . 5 class 𝑛
6 czn 19615 . . . . 5 class ℤ/n
75, 6cfv 5790 . . . 4 class (ℤ/nℤ‘𝑛)
8 vb . . . . 5 setvar 𝑏
94cv 1473 . . . . . . . . . 10 class 𝑧
10 cbs 15641 . . . . . . . . . 10 class Base
119, 10cfv 5790 . . . . . . . . 9 class (Base‘𝑧)
12 cui 18408 . . . . . . . . . 10 class Unit
139, 12cfv 5790 . . . . . . . . 9 class (Unit‘𝑧)
1411, 13cdif 3536 . . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15 cc0 9792 . . . . . . . . 9 class 0
1615csn 4124 . . . . . . . 8 class {0}
1714, 16cxp 5026 . . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18 vx . . . . . . . 8 setvar 𝑥
1918cv 1473 . . . . . . 7 class 𝑥
2017, 19wss 3539 . . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21 cmgp 18258 . . . . . . . 8 class mulGrp
229, 21cfv 5790 . . . . . . 7 class (mulGrp‘𝑧)
23 ccnfld 19513 . . . . . . . 8 class fld
2423, 21cfv 5790 . . . . . . 7 class (mulGrp‘ℂfld)
25 cmhm 17102 . . . . . . 7 class MndHom
2622, 24, 25co 6527 . . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
2720, 18, 26crab 2899 . . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28 cnx 15638 . . . . . . . 8 class ndx
2928, 10cfv 5790 . . . . . . 7 class (Base‘ndx)
308cv 1473 . . . . . . 7 class 𝑏
3129, 30cop 4130 . . . . . 6 class ⟨(Base‘ndx), 𝑏
32 cplusg 15714 . . . . . . . 8 class +g
3328, 32cfv 5790 . . . . . . 7 class (+g‘ndx)
34 cmul 9797 . . . . . . . . 9 class ·
3534cof 6770 . . . . . . . 8 class 𝑓 ·
3630, 30cxp 5026 . . . . . . . 8 class (𝑏 × 𝑏)
3735, 36cres 5030 . . . . . . 7 class ( ∘𝑓 · ↾ (𝑏 × 𝑏))
3833, 37cop 4130 . . . . . 6 class ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩
3931, 38cpr 4126 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
408, 27, 39csb 3498 . . . 4 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
414, 7, 40csb 3498 . . 3 class (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
422, 3, 41cmpt 4637 . 2 class (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})
431, 42wceq 1474 1 wff DChr = (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  dchrval  24676  dchrrcl  24682
  Copyright terms: Public domain W3C validator