Definition df-dchr 27196

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 27195	. 2 class DChr
2		vn	. . 3 setvar 𝑛
3		cn 12242	. . 3 class ℕ
4		vz	. . . 4 setvar 𝑧
5	2	cv 1532	. . . . 5 class 𝑛
6		czn 21432	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 6547	. . . 4 class (ℤ/nℤ‘𝑛)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1532	. . . . . . . . . 10 class 𝑧
10		cbs 17179	. . . . . . . . . 10 class Base
11	9, 10	cfv 6547	. . . . . . . . 9 class (Base‘𝑧)
12		cui 20298	. . . . . . . . . 10 class Unit
13	9, 12	cfv 6547	. . . . . . . . 9 class (Unit‘𝑧)
14	11, 13	cdif 3942	. . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15		cc0 11138	. . . . . . . . 9 class 0
16	15	csn 4629	. . . . . . . 8 class {0}
17	14, 16	cxp 5675	. . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1532	. . . . . . 7 class 𝑥
20	17, 19	wss 3945	. . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21		cmgp 20078	. . . . . . . 8 class mulGrp
22	9, 21	cfv 6547	. . . . . . 7 class (mulGrp‘𝑧)
23		ccnfld 21283	. . . . . . . 8 class ℂfld
24	23, 21	cfv 6547	. . . . . . 7 class (mulGrp‘ℂfld)
25		cmhm 18737	. . . . . . 7 class MndHom
26	22, 24, 25	co 7417	. . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
27	20, 18, 26	crab 3419	. . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28		cnx 17161	. . . . . . . 8 class ndx
29	28, 10	cfv 6547	. . . . . . 7 class (Base‘ndx)
30	8	cv 1532	. . . . . . 7 class 𝑏
31	29, 30	cop 4635	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
32		cplusg 17232	. . . . . . . 8 class +g
33	28, 32	cfv 6547	. . . . . . 7 class (+g‘ndx)
34		cmul 11143	. . . . . . . . 9 class ·
35	34	cof 7681	. . . . . . . 8 class ∘f ·
36	30, 30	cxp 5675	. . . . . . . 8 class (𝑏 × 𝑏)
37	35, 36	cres 5679	. . . . . . 7 class ( ∘f · ↾ (𝑏 × 𝑏))
38	33, 37	cop 4635	. . . . . 6 class ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩
39	31, 38	cpr 4631	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
40	8, 27, 39	csb 3890	. . . 4 class ⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
41	4, 7, 40	csb 3890	. . 3 class ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩}
42	2, 3, 41	cmpt 5231	. 2 class (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
43	1, 42	wceq 1533	1 wff DChr = (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})

This definition is referenced by:  dchrval  27197  dchrrcl  27203