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

Definition df-dchr 25820
 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 25819 . 2 class DChr
2 vn . . 3 setvar 𝑛
3 cn 11629 . . 3 class
4 vz . . . 4 setvar 𝑧
52cv 1537 . . . . 5 class 𝑛
6 czn 20199 . . . . 5 class ℤ/n
75, 6cfv 6328 . . . 4 class (ℤ/nℤ‘𝑛)
8 vb . . . . 5 setvar 𝑏
94cv 1537 . . . . . . . . . 10 class 𝑧
10 cbs 16478 . . . . . . . . . 10 class Base
119, 10cfv 6328 . . . . . . . . 9 class (Base‘𝑧)
12 cui 19388 . . . . . . . . . 10 class Unit
139, 12cfv 6328 . . . . . . . . 9 class (Unit‘𝑧)
1411, 13cdif 3881 . . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15 cc0 10530 . . . . . . . . 9 class 0
1615csn 4528 . . . . . . . 8 class {0}
1714, 16cxp 5521 . . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18 vx . . . . . . . 8 setvar 𝑥
1918cv 1537 . . . . . . 7 class 𝑥
2017, 19wss 3884 . . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21 cmgp 19235 . . . . . . . 8 class mulGrp
229, 21cfv 6328 . . . . . . 7 class (mulGrp‘𝑧)
23 ccnfld 20094 . . . . . . . 8 class fld
2423, 21cfv 6328 . . . . . . 7 class (mulGrp‘ℂfld)
25 cmhm 17949 . . . . . . 7 class MndHom
2622, 24, 25co 7139 . . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
2720, 18, 26crab 3113 . . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28 cnx 16475 . . . . . . . 8 class ndx
2928, 10cfv 6328 . . . . . . 7 class (Base‘ndx)
308cv 1537 . . . . . . 7 class 𝑏
3129, 30cop 4534 . . . . . 6 class ⟨(Base‘ndx), 𝑏
32 cplusg 16560 . . . . . . . 8 class +g
3328, 32cfv 6328 . . . . . . 7 class (+g‘ndx)
34 cmul 10535 . . . . . . . . 9 class ·
3534cof 7391 . . . . . . . 8 class f ·
3630, 30cxp 5521 . . . . . . . 8 class (𝑏 × 𝑏)
3735, 36cres 5525 . . . . . . 7 class ( ∘f · ↾ (𝑏 × 𝑏))
3833, 37cop 4534 . . . . . 6 class ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩
3931, 38cpr 4530 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
408, 27, 39csb 3831 . . . 4 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
414, 7, 40csb 3831 . . 3 class (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
422, 3, 41cmpt 5113 . 2 class (𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑛) / 𝑧{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
431, 42wceq 1538 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  25821  dchrrcl  25827
 Copyright terms: Public domain W3C validator