Metamath Proof Explorer

Theorem dchrghm

Description: A Dirichlet character restricted to the unit group of Z/nZ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses dchrghm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrghm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrghm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrghm.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrghm.h ⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
dchrghm.m ⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
dchrghm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion dchrghm ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 GrpHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 dchrghm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrghm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrghm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrghm.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 dchrghm.h ⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
6 dchrghm.m ⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
7 dchrghm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 1 2 3 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
9 8 7 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
10 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
11 7 10 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12 11 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
13 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
14 12 13 syl ⊢ ( 𝜑 → 𝑍 ∈ CRing )
15 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
16 14 15 syl ⊢ ( 𝜑 → 𝑍 ∈ Ring )
17 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
18 4 17 unitsubm ⊢ ( 𝑍 ∈ Ring → 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) )
19 16 18 syl ⊢ ( 𝜑 → 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) )
20 5 resmhm ⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) ) → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂfld ) ) )
21 9 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂfld ) ) )
22 cnring ⊢ ℂfld ∈ Ring
23 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
24 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
25 cndrng ⊢ ℂfld ∈ DivRing
26 23 24 25 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
27 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
28 26 27 unitsubm ⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
29 22 28 ax-mp ⊢ ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
30 df-ima ⊢ ( 𝑋 “ 𝑈 ) = ran ( 𝑋 ↾ 𝑈 )
31 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
32 1 2 3 31 7 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
33 31 4 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
34 33 sseli ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑍 ) )
35 ffvelrn ⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
36 32 34 35 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
38 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑋 ∈ 𝐷 )
39 34 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑍 ) )
40 1 2 3 31 4 38 39 dchrn0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ 𝑥 ∈ 𝑈 ) )
41 37 40 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ≠ 0 )
42 eldifsn ⊢ ( ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) )
43 36 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
45 32 ffund ⊢ ( 𝜑 → Fun 𝑋 )
46 32 fdmd ⊢ ( 𝜑 → dom 𝑋 = ( Base ‘ 𝑍 ) )
47 33 46 sseqtrrid ⊢ ( 𝜑 → 𝑈 ⊆ dom 𝑋 )
48 funimass4 ⊢ ( ( Fun 𝑋 ∧ 𝑈 ⊆ dom 𝑋 ) → ( ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
49 45 47 48 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
50 44 49 mpbird ⊢ ( 𝜑 → ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) )
51 30 50 eqsstrrid ⊢ ( 𝜑 → ran ( 𝑋 ↾ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) )
52 6 resmhm2b ⊢ ( ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ ran ( 𝑋 ↾ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂfld ) ) ↔ ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) ) )
53 29 51 52 sylancr ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂfld ) ) ↔ ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) ) )
54 21 53 mpbid ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) )
55 4 5 unitgrp ⊢ ( 𝑍 ∈ Ring → 𝐻 ∈ Grp )
56 16 55 syl ⊢ ( 𝜑 → 𝐻 ∈ Grp )
57 6 cnmgpabl ⊢ 𝑀 ∈ Abel
58 ablgrp ⊢ ( 𝑀 ∈ Abel → 𝑀 ∈ Grp )
59 57 58 ax-mp ⊢ 𝑀 ∈ Grp
60 ghmmhmb ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑀 ∈ Grp ) → ( 𝐻 GrpHom 𝑀 ) = ( 𝐻 MndHom 𝑀 ) )
61 56 59 60 sylancl ⊢ ( 𝜑 → ( 𝐻 GrpHom 𝑀 ) = ( 𝐻 MndHom 𝑀 ) )
62 54 61 eleqtrrd ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 GrpHom 𝑀 ) )