Definition df-dchr 26381

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

Step	Hyp	Ref	Expression
1		cdchr 26380	. 2 class DChr
2		vn	. . 3 setvar 𝑛
3		cn 11973	. . 3 class ℕ
4		vz	. . . 4 setvar 𝑧
5	2	cv 1538	. . . . 5 class 𝑛
6		czn 20704	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 6433	. . . 4 class (ℤ/nℤ‘𝑛)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1538	. . . . . . . . . 10 class 𝑧
10		cbs 16912	. . . . . . . . . 10 class Base
11	9, 10	cfv 6433	. . . . . . . . 9 class (Base‘𝑧)
12		cui 19881	. . . . . . . . . 10 class Unit
13	9, 12	cfv 6433	. . . . . . . . 9 class (Unit‘𝑧)
14	11, 13	cdif 3884	. . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15		cc0 10871	. . . . . . . . 9 class 0
16	15	csn 4561	. . . . . . . 8 class {0}
17	14, 16	cxp 5587	. . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1538	. . . . . . 7 class 𝑥
20	17, 19	wss 3887	. . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21		cmgp 19720	. . . . . . . 8 class mulGrp
22	9, 21	cfv 6433	. . . . . . 7 class (mulGrp‘𝑧)
23		ccnfld 20597	. . . . . . . 8 class ℂfld
24	23, 21	cfv 6433	. . . . . . 7 class (mulGrp‘ℂfld)
25		cmhm 18428	. . . . . . 7 class MndHom
26	22, 24, 25	co 7275	. . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
27	20, 18, 26	crab 3068	. . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28		cnx 16894	. . . . . . . 8 class ndx
29	28, 10	cfv 6433	. . . . . . 7 class (Base‘ndx)
30	8	cv 1538	. . . . . . 7 class 𝑏
31	29, 30	cop 4567	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
32		cplusg 16962	. . . . . . . 8 class +g
33	28, 32	cfv 6433	. . . . . . 7 class (+g‘ndx)
34		cmul 10876	. . . . . . . . 9 class ·
35	34	cof 7531	. . . . . . . 8 class ∘f ·
36	30, 30	cxp 5587	. . . . . . . 8 class (𝑏 × 𝑏)
37	35, 36	cres 5591	. . . . . . 7 class ( ∘f · ↾ (𝑏 × 𝑏))
38	33, 37	cop 4567	. . . . . 6 class ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩
39	31, 38	cpr 4563	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
40	8, 27, 39	csb 3832	. . . 4 class ⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
41	4, 7, 40	csb 3832	. . 3 class ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
42	2, 3, 41	cmpt 5157	. 2 class (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
43	1, 42	wceq 1539	1 wff DChr = (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})

This definition is referenced by:  dchrval  26382  dchrrcl  26388