Definition df-dchr 24958

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

Step	Hyp	Ref	Expression
1		cdchr 24957	. 2 class DChr
2		vn	. . 3 setvar 𝑛
3		cn 11020	. . 3 class ℕ
4		vz	. . . 4 setvar 𝑧
5	2	cv 1482	. . . . 5 class 𝑛
6		czn 19851	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 5888	. . . 4 class (ℤ/nℤ‘𝑛)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1482	. . . . . . . . . 10 class 𝑧
10		cbs 15857	. . . . . . . . . 10 class Base
11	9, 10	cfv 5888	. . . . . . . . 9 class (Base‘𝑧)
12		cui 18639	. . . . . . . . . 10 class Unit
13	9, 12	cfv 5888	. . . . . . . . 9 class (Unit‘𝑧)
14	11, 13	cdif 3571	. . . . . . . 8 class ((Base‘𝑧) ∖ (Unit‘𝑧))
15		cc0 9936	. . . . . . . . 9 class 0
16	15	csn 4177	. . . . . . . 8 class {0}
17	14, 16	cxp 5112	. . . . . . 7 class (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0})
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1482	. . . . . . 7 class 𝑥
20	17, 19	wss 3574	. . . . . 6 wff (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥
21		cmgp 18489	. . . . . . . 8 class mulGrp
22	9, 21	cfv 5888	. . . . . . 7 class (mulGrp‘𝑧)
23		ccnfld 19746	. . . . . . . 8 class ℂfld
24	23, 21	cfv 5888	. . . . . . 7 class (mulGrp‘ℂfld)
25		cmhm 17333	. . . . . . 7 class MndHom
26	22, 24, 25	co 6650	. . . . . 6 class ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld))
27	20, 18, 26	crab 2916	. . . . 5 class {𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥}
28		cnx 15854	. . . . . . . 8 class ndx
29	28, 10	cfv 5888	. . . . . . 7 class (Base‘ndx)
30	8	cv 1482	. . . . . . 7 class 𝑏
31	29, 30	cop 4183	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
32		cplusg 15941	. . . . . . . 8 class +g
33	28, 32	cfv 5888	. . . . . . 7 class (+g‘ndx)
34		cmul 9941	. . . . . . . . 9 class ·
35	34	cof 6895	. . . . . . . 8 class ∘𝑓 ·
36	30, 30	cxp 5112	. . . . . . . 8 class (𝑏 × 𝑏)
37	35, 36	cres 5116	. . . . . . 7 class ( ∘𝑓 · ↾ (𝑏 × 𝑏))
38	33, 37	cop 4183	. . . . . 6 class ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩
39	31, 38	cpr 4179	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
40	8, 27, 39	csb 3533	. . . 4 class ⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
41	4, 7, 40	csb 3533	. . 3 class ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩}
42	2, 3, 41	cmpt 4729	. 2 class (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})
43	1, 42	wceq 1483	1 wff DChr = (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 · ↾ (𝑏 × 𝑏))⟩})

This definition is referenced by:  dchrval  24959  dchrrcl  24965