Metamath Proof Explorer

Theorem dchrzrhmul

Description: A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses dchrmhm.g 
|- G = ( DChr ` N )
dchrmhm.z 
|- Z = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrelbas4.l 
|- L = ( ZRHom ` Z )
dchrzrh1.x 
|- ( ph -> X e. D )
dchrzrh1.a 
|- ( ph -> A e. ZZ )
dchrzrh1.c 
|- ( ph -> C e. ZZ )
Assertion dchrzrhmul 
|- ( ph -> ( X ` ( L ` ( A x. C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 
 |-  G = ( DChr ` N )
2 dchrmhm.z 
 |-  Z = ( Z/nZ ` N )
3 dchrmhm.b 
 |-  D = ( Base ` G )
4 dchrelbas4.l 
 |-  L = ( ZRHom ` Z )
5 dchrzrh1.x 
 |-  ( ph -> X e. D )
6 dchrzrh1.a 
 |-  ( ph -> A e. ZZ )
7 dchrzrh1.c 
 |-  ( ph -> C e. ZZ )
8 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
9 5 8 syl 
 |-  ( ph -> N e. NN )
10 9 nnnn0d 
 |-  ( ph -> N e. NN0 )
11 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
12 10 11 syl 
 |-  ( ph -> Z e. CRing )
13 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
14 12 13 syl 
 |-  ( ph -> Z e. Ring )
15 4 zrhrhm 
 |-  ( Z e. Ring -> L e. ( ZZring RingHom Z ) )
16 14 15 syl 
 |-  ( ph -> L e. ( ZZring RingHom Z ) )
17 zringbas 
 |-  ZZ = ( Base ` ZZring )
18 zringmulr 
 |-  x. = ( .r ` ZZring )
19 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
20 17 18 19 rhmmul 
 |-  ( ( L e. ( ZZring RingHom Z ) /\ A e. ZZ /\ C e. ZZ ) -> ( L ` ( A x. C ) ) = ( ( L ` A ) ( .r ` Z ) ( L ` C ) ) )
21 16 6 7 20 syl3anc 
 |-  ( ph -> ( L ` ( A x. C ) ) = ( ( L ` A ) ( .r ` Z ) ( L ` C ) ) )
22 21 fveq2d 
 |-  ( ph -> ( X ` ( L ` ( A x. C ) ) ) = ( X ` ( ( L ` A ) ( .r ` Z ) ( L ` C ) ) ) )
23 1 2 3 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
24 23 5 sseldi 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
25 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
26 17 25 rhmf 
 |-  ( L e. ( ZZring RingHom Z ) -> L : ZZ --> ( Base ` Z ) )
27 16 26 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
28 27 6 ffvelrnd 
 |-  ( ph -> ( L ` A ) e. ( Base ` Z ) )
29 27 7 ffvelrnd 
 |-  ( ph -> ( L ` C ) e. ( Base ` Z ) )
30 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
31 30 25 mgpbas 
 |-  ( Base ` Z ) = ( Base ` ( mulGrp ` Z ) )
32 30 19 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
33 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
34 cnfldmul 
 |-  x. = ( .r ` CCfld )
35 33 34 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
36 31 32 35 mhmlin 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( L ` A ) e. ( Base ` Z ) /\ ( L ` C ) e. ( Base ` Z ) ) -> ( X ` ( ( L ` A ) ( .r ` Z ) ( L ` C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )
37 24 28 29 36 syl3anc 
 |-  ( ph -> ( X ` ( ( L ` A ) ( .r ` Z ) ( L ` C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )
38 22 37 eqtrd 
 |-  ( ph -> ( X ` ( L ` ( A x. C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )