Definition df-dchr

Description: The group of Dirichlet characters mod n is the set of monoid homomorphisms from ZZ / n ZZ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Assertion	df-dchr	⊢ DChr = ( 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdchr	⊢ DChr
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		czn	⊢ ℤ/nℤ
4	1	cv	⊢ 𝑛
5	4 3	cfv	⊢ ( ℤ/nℤ ‘ 𝑛 )
6		vz	⊢ 𝑧
7		vx	⊢ 𝑥
8		cmgp	⊢ mulGrp
9	6	cv	⊢ 𝑧
10	9 8	cfv	⊢ ( mulGrp ‘ 𝑧 )
11		cmhm	⊢ MndHom
12		ccnfld	⊢ ℂfld
13	12 8	cfv	⊢ ( mulGrp ‘ ℂfld )
14	10 13 11	co	⊢ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) )
15		cbs	⊢ Base
16	9 15	cfv	⊢ ( Base ‘ 𝑧 )
17		cui	⊢ Unit
18	9 17	cfv	⊢ ( Unit ‘ 𝑧 )
19	16 18	cdif	⊢ ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) )
20		cc0	⊢ 0
21	20	csn	⊢ { 0 }
22	19 21	cxp	⊢ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } )
23	7	cv	⊢ 𝑥
24	22 23	wss	⊢ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥
25	24 7 14	crab	⊢ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 }
26		vb	⊢ 𝑏
27		cnx	⊢ ndx
28	27 15	cfv	⊢ ( Base ‘ ndx )
29	26	cv	⊢ 𝑏
30	28 29	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
31		cplusg	⊢ +g
32	27 31	cfv	⊢ ( +g ‘ ndx )
33		cmul	⊢ ·
34	33	cof	⊢ ∘f ·
35	29 29	cxp	⊢ ( 𝑏 × 𝑏 )
36	34 35	cres	⊢ ( ∘f · ↾ ( 𝑏 × 𝑏 ) )
37	32 36	cop	⊢ ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩
38	30 37	cpr	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ }
39	26 25 38	csb	⊢ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ }
40	6 5 39	csb	⊢ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ }
41	1 2 40	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )
42	0 41	wceq	⊢ DChr = ( 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )