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 26379
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 26378 . 2 class DChr
2 vn . . 3 setvar 𝑛
3 cn 11971 . . 3 class
4 vz . . . 4 setvar 𝑧
52cv 1538 . . . . 5 class 𝑛
6 czn 20702 . . . . 5 class ℤ/n
75, 6cfv 6435 . . . 4 class (ℤ/nℤ‘𝑛)
8 vb . . . . 5 setvar 𝑏
94cv 1538 . . . . . . . . . 10 class 𝑧
10 cbs 16910 . . . . . . . . . 10 class Base
119, 10cfv 6435 . . . . . . . . 9 class (Base‘𝑧)
12 cui 19879 . . . . . . . . . 10 class Unit
139, 12cfv 6435 . . . . . . . . 9 class (Unit‘𝑧)
1411, 13cdif 3885 . . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15 cc0 10869 . . . . . . . . 9 class 0
1615csn 4563 . . . . . . . 8 class {0}
1714, 16cxp 5589 . . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18 vx . . . . . . . 8 setvar 𝑥
1918cv 1538 . . . . . . 7 class 𝑥
2017, 19wss 3888 . . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21 cmgp 19718 . . . . . . . 8 class mulGrp
229, 21cfv 6435 . . . . . . 7 class (mulGrp‘𝑧)
23 ccnfld 20595 . . . . . . . 8 class fld
2423, 21cfv 6435 . . . . . . 7 class (mulGrp‘ℂfld)
25 cmhm 18426 . . . . . . 7 class MndHom
2622, 24, 25co 7277 . . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
2720, 18, 26crab 3068 . . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28 cnx 16892 . . . . . . . 8 class ndx
2928, 10cfv 6435 . . . . . . 7 class (Base‘ndx)
308cv 1538 . . . . . . 7 class 𝑏
3129, 30cop 4569 . . . . . 6 class ⟨(Base‘ndx), 𝑏
32 cplusg 16960 . . . . . . . 8 class +g
3328, 32cfv 6435 . . . . . . 7 class (+g‘ndx)
34 cmul 10874 . . . . . . . . 9 class ·
3534cof 7531 . . . . . . . 8 class f ·
3630, 30cxp 5589 . . . . . . . 8 class (𝑏 × 𝑏)
3735, 36cres 5593 . . . . . . 7 class ( ∘f · ↾ (𝑏 × 𝑏))
3833, 37cop 4569 . . . . . 6 class ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩
3931, 38cpr 4565 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
408, 27, 39csb 3833 . . . 4 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
414, 7, 40csb 3833 . . 3 class (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
422, 3, 41cmpt 5159 . 2 class (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
431, 42wceq 1539 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  26380  dchrrcl  26386
  Copyright terms: Public domain W3C validator