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 25736
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), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
Distinct variable groups:   𝑥,𝑧   𝑛,𝑏,𝑧,𝑥

Detailed syntax breakdown of Definition df-dchr
StepHypRef Expression
1 cdchr 25735 . 2 class DChr
2 vn . . 3 setvar 𝑛
3 cn 11626 . . 3 class
4 vz . . . 4 setvar 𝑧
52cv 1527 . . . . 5 class 𝑛
6 czn 20578 . . . . 5 class ℤ/n
75, 6cfv 6348 . . . 4 class (ℤ/nℤ‘𝑛)
8 vb . . . . 5 setvar 𝑏
94cv 1527 . . . . . . . . . 10 class 𝑧
10 cbs 16471 . . . . . . . . . 10 class Base
119, 10cfv 6348 . . . . . . . . 9 class (Base‘𝑧)
12 cui 19318 . . . . . . . . . 10 class Unit
139, 12cfv 6348 . . . . . . . . 9 class (Unit‘𝑧)
1411, 13cdif 3930 . . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15 cc0 10525 . . . . . . . . 9 class 0
1615csn 4557 . . . . . . . 8 class {0}
1714, 16cxp 5546 . . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18 vx . . . . . . . 8 setvar 𝑥
1918cv 1527 . . . . . . 7 class 𝑥
2017, 19wss 3933 . . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21 cmgp 19168 . . . . . . . 8 class mulGrp
229, 21cfv 6348 . . . . . . 7 class (mulGrp‘𝑧)
23 ccnfld 20473 . . . . . . . 8 class fld
2423, 21cfv 6348 . . . . . . 7 class (mulGrp‘ℂfld)
25 cmhm 17942 . . . . . . 7 class MndHom
2622, 24, 25co 7145 . . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
2720, 18, 26crab 3139 . . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28 cnx 16468 . . . . . . . 8 class ndx
2928, 10cfv 6348 . . . . . . 7 class (Base‘ndx)
308cv 1527 . . . . . . 7 class 𝑏
3129, 30cop 4563 . . . . . 6 class ⟨(Base‘ndx), 𝑏
32 cplusg 16553 . . . . . . . 8 class +g
3328, 32cfv 6348 . . . . . . 7 class (+g‘ndx)
34 cmul 10530 . . . . . . . . 9 class ·
3534cof 7396 . . . . . . . 8 class f ·
3630, 30cxp 5546 . . . . . . . 8 class (𝑏 × 𝑏)
3735, 36cres 5550 . . . . . . 7 class ( ∘f · ↾ (𝑏 × 𝑏))
3833, 37cop 4563 . . . . . 6 class ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩
3931, 38cpr 4559 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
408, 27, 39csb 3880 . . . 4 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
414, 7, 40csb 3880 . . 3 class (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
422, 3, 41cmpt 5137 . 2 class (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
431, 42wceq 1528 1 wff DChr = (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  dchrval  25737  dchrrcl  25743
  Copyright terms: Public domain W3C validator