This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )