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 25003
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 25002 . 2 class DChr
2 vn . . 3 setvar 𝑛
3 cn 11058 . . 3 class
4 vz . . . 4 setvar 𝑧
52cv 1522 . . . . 5 class 𝑛
6 czn 19899 . . . . 5 class ℤ/n
75, 6cfv 5926 . . . 4 class (ℤ/nℤ‘𝑛)
8 vb . . . . 5 setvar 𝑏
94cv 1522 . . . . . . . . . 10 class 𝑧
10 cbs 15904 . . . . . . . . . 10 class Base
119, 10cfv 5926 . . . . . . . . 9 class (Base‘𝑧)
12 cui 18685 . . . . . . . . . 10 class Unit
139, 12cfv 5926 . . . . . . . . 9 class (Unit‘𝑧)
1411, 13cdif 3604 . . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15 cc0 9974 . . . . . . . . 9 class 0
1615csn 4210 . . . . . . . 8 class {0}
1714, 16cxp 5141 . . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18 vx . . . . . . . 8 setvar 𝑥
1918cv 1522 . . . . . . 7 class 𝑥
2017, 19wss 3607 . . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21 cmgp 18535 . . . . . . . 8 class mulGrp
229, 21cfv 5926 . . . . . . 7 class (mulGrp‘𝑧)
23 ccnfld 19794 . . . . . . . 8 class fld
2423, 21cfv 5926 . . . . . . 7 class (mulGrp‘ℂfld)
25 cmhm 17380 . . . . . . 7 class MndHom
2622, 24, 25co 6690 . . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
2720, 18, 26crab 2945 . . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28 cnx 15901 . . . . . . . 8 class ndx
2928, 10cfv 5926 . . . . . . 7 class (Base‘ndx)
308cv 1522 . . . . . . 7 class 𝑏
3129, 30cop 4216 . . . . . 6 class ⟨(Base‘ndx), 𝑏
32 cplusg 15988 . . . . . . . 8 class +g
3328, 32cfv 5926 . . . . . . 7 class (+g‘ndx)
34 cmul 9979 . . . . . . . . 9 class ·
3534cof 6937 . . . . . . . 8 class 𝑓 ·
3630, 30cxp 5141 . . . . . . . 8 class (𝑏 × 𝑏)
3735, 36cres 5145 . . . . . . 7 class ( ∘𝑓 · ↾ (𝑏 × 𝑏))
3833, 37cop 4216 . . . . . 6 class ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩
3931, 38cpr 4212 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
408, 27, 39csb 3566 . . . 4 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
414, 7, 40csb 3566 . . 3 class (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
422, 3, 41cmpt 4762 . 2 class (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})
431, 42wceq 1523 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  25004  dchrrcl  25010
  Copyright terms: Public domain W3C validator