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 
|- G = ( DChr ` N )
dchrghm.z 
|- Z = ( Z/nZ ` N )
dchrghm.b 
|- D = ( Base ` G )
dchrghm.u 
|- U = ( Unit ` Z )
dchrghm.h 
|- H = ( ( mulGrp ` Z ) |`s U )
dchrghm.m 
|- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
dchrghm.x 
|- ( ph -> X e. D )
Assertion dchrghm 
|- ( ph -> ( X |` U ) e. ( H GrpHom M ) )

Proof

Step Hyp Ref Expression
1 dchrghm.g 
 |-  G = ( DChr ` N )
2 dchrghm.z 
 |-  Z = ( Z/nZ ` N )
3 dchrghm.b 
 |-  D = ( Base ` G )
4 dchrghm.u 
 |-  U = ( Unit ` Z )
5 dchrghm.h 
 |-  H = ( ( mulGrp ` Z ) |`s U )
6 dchrghm.m 
 |-  M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
7 dchrghm.x 
 |-  ( ph -> X e. D )
8 1 2 3 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
9 8 7 sseldi 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
10 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
11 7 10 syl 
 |-  ( ph -> N e. NN )
12 11 nnnn0d 
 |-  ( ph -> N e. NN0 )
13 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
14 12 13 syl 
 |-  ( ph -> Z e. CRing )
15 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
16 14 15 syl 
 |-  ( ph -> Z e. Ring )
17 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
18 4 17 unitsubm 
 |-  ( Z e. Ring -> U e. ( SubMnd ` ( mulGrp ` Z ) ) )
19 16 18 syl 
 |-  ( ph -> U e. ( SubMnd ` ( mulGrp ` Z ) ) )
20 5 resmhm 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ U e. ( SubMnd ` ( mulGrp ` Z ) ) ) -> ( X |` U ) e. ( H MndHom ( mulGrp ` CCfld ) ) )
21 9 19 20 syl2anc 
 |-  ( ph -> ( X |` U ) e. ( H MndHom ( mulGrp ` CCfld ) ) )
22 cnring 
 |-  CCfld e. Ring
23 cnfldbas 
 |-  CC = ( Base ` CCfld )
24 cnfld0 
 |-  0 = ( 0g ` CCfld )
25 cndrng 
 |-  CCfld e. DivRing
26 23 24 25 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
27 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
28 26 27 unitsubm 
 |-  ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
29 22 28 ax-mp 
 |-  ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) )
30 df-ima 
 |-  ( X " U ) = ran ( X |` U )
31 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
32 1 2 3 31 7 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
33 31 4 unitss 
 |-  U C_ ( Base ` Z )
34 33 sseli 
 |-  ( x e. U -> x e. ( Base ` Z ) )
35 ffvelrn 
 |-  ( ( X : ( Base ` Z ) --> CC /\ x e. ( Base ` Z ) ) -> ( X ` x ) e. CC )
36 32 34 35 syl2an 
 |-  ( ( ph /\ x e. U ) -> ( X ` x ) e. CC )
37 simpr 
 |-  ( ( ph /\ x e. U ) -> x e. U )
38 7 adantr 
 |-  ( ( ph /\ x e. U ) -> X e. D )
39 34 adantl 
 |-  ( ( ph /\ x e. U ) -> x e. ( Base ` Z ) )
40 1 2 3 31 4 38 39 dchrn0 
 |-  ( ( ph /\ x e. U ) -> ( ( X ` x ) =/= 0 <-> x e. U ) )
41 37 40 mpbird 
 |-  ( ( ph /\ x e. U ) -> ( X ` x ) =/= 0 )
42 eldifsn 
 |-  ( ( X ` x ) e. ( CC \ { 0 } ) <-> ( ( X ` x ) e. CC /\ ( X ` x ) =/= 0 ) )
43 36 41 42 sylanbrc 
 |-  ( ( ph /\ x e. U ) -> ( X ` x ) e. ( CC \ { 0 } ) )
44 43 ralrimiva 
 |-  ( ph -> A. x e. U ( X ` x ) e. ( CC \ { 0 } ) )
45 32 ffund 
 |-  ( ph -> Fun X )
46 32 fdmd 
 |-  ( ph -> dom X = ( Base ` Z ) )
47 33 46 sseqtrrid 
 |-  ( ph -> U C_ dom X )
48 funimass4 
 |-  ( ( Fun X /\ U C_ dom X ) -> ( ( X " U ) C_ ( CC \ { 0 } ) <-> A. x e. U ( X ` x ) e. ( CC \ { 0 } ) ) )
49 45 47 48 syl2anc 
 |-  ( ph -> ( ( X " U ) C_ ( CC \ { 0 } ) <-> A. x e. U ( X ` x ) e. ( CC \ { 0 } ) ) )
50 44 49 mpbird 
 |-  ( ph -> ( X " U ) C_ ( CC \ { 0 } ) )
51 30 50 eqsstrrid 
 |-  ( ph -> ran ( X |` U ) C_ ( CC \ { 0 } ) )
52 6 resmhm2b 
 |-  ( ( ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ran ( X |` U ) C_ ( CC \ { 0 } ) ) -> ( ( X |` U ) e. ( H MndHom ( mulGrp ` CCfld ) ) <-> ( X |` U ) e. ( H MndHom M ) ) )
53 29 51 52 sylancr 
 |-  ( ph -> ( ( X |` U ) e. ( H MndHom ( mulGrp ` CCfld ) ) <-> ( X |` U ) e. ( H MndHom M ) ) )
54 21 53 mpbid 
 |-  ( ph -> ( X |` U ) e. ( H MndHom M ) )
55 4 5 unitgrp 
 |-  ( Z e. Ring -> H e. Grp )
56 16 55 syl 
 |-  ( ph -> H e. Grp )
57 6 cnmgpabl 
 |-  M e. Abel
58 ablgrp 
 |-  ( M e. Abel -> M e. Grp )
59 57 58 ax-mp 
 |-  M e. Grp
60 ghmmhmb 
 |-  ( ( H e. Grp /\ M e. Grp ) -> ( H GrpHom M ) = ( H MndHom M ) )
61 56 59 60 sylancl 
 |-  ( ph -> ( H GrpHom M ) = ( H MndHom M ) )
62 54 61 eleqtrrd 
 |-  ( ph -> ( X |` U ) e. ( H GrpHom M ) )