Metamath Proof Explorer

Theorem dchrisum0fmul

Description: The function F , the divisor sum of a Dirichlet character, is a multiplicative function (but not completely multiplicative). Equation 9.4.27 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
dchrisum0f.f 
|- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
dchrisum0f.x 
|- ( ph -> X e. D )
dchrisum0fmul.a 
|- ( ph -> A e. NN )
dchrisum0fmul.b 
|- ( ph -> B e. NN )
dchrisum0fmul.m 
|- ( ph -> ( A gcd B ) = 1 )
Assertion dchrisum0fmul 
|- ( ph -> ( F ` ( A x. B ) ) = ( ( F ` A ) x. ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 dchrisum0f.f 
 |-  F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
8 dchrisum0f.x 
 |-  ( ph -> X e. D )
9 dchrisum0fmul.a 
 |-  ( ph -> A e. NN )
10 dchrisum0fmul.b 
 |-  ( ph -> B e. NN )
11 dchrisum0fmul.m 
 |-  ( ph -> ( A gcd B ) = 1 )
12 eqid 
 |-  { q e. NN | q || A } = { q e. NN | q || A }
13 eqid 
 |-  { q e. NN | q || B } = { q e. NN | q || B }
14 eqid 
 |-  { q e. NN | q || ( A x. B ) } = { q e. NN | q || ( A x. B ) }
15 8 adantr 
 |-  ( ( ph /\ j e. { q e. NN | q || A } ) -> X e. D )
16 elrabi 
 |-  ( j e. { q e. NN | q || A } -> j e. NN )
17 16 nnzd 
 |-  ( j e. { q e. NN | q || A } -> j e. ZZ )
18 17 adantl 
 |-  ( ( ph /\ j e. { q e. NN | q || A } ) -> j e. ZZ )
19 4 1 5 2 15 18 dchrzrhcl 
 |-  ( ( ph /\ j e. { q e. NN | q || A } ) -> ( X ` ( L ` j ) ) e. CC )
20 8 adantr 
 |-  ( ( ph /\ k e. { q e. NN | q || B } ) -> X e. D )
21 elrabi 
 |-  ( k e. { q e. NN | q || B } -> k e. NN )
22 21 nnzd 
 |-  ( k e. { q e. NN | q || B } -> k e. ZZ )
23 22 adantl 
 |-  ( ( ph /\ k e. { q e. NN | q || B } ) -> k e. ZZ )
24 4 1 5 2 20 23 dchrzrhcl 
 |-  ( ( ph /\ k e. { q e. NN | q || B } ) -> ( X ` ( L ` k ) ) e. CC )
25 17 22 anim12i 
 |-  ( ( j e. { q e. NN | q || A } /\ k e. { q e. NN | q || B } ) -> ( j e. ZZ /\ k e. ZZ ) )
26 8 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ k e. ZZ ) ) -> X e. D )
27 simprl 
 |-  ( ( ph /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. ZZ )
28 simprr 
 |-  ( ( ph /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. ZZ )
29 4 1 5 2 26 27 28 dchrzrhmul 
 |-  ( ( ph /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( X ` ( L ` ( j x. k ) ) ) = ( ( X ` ( L ` j ) ) x. ( X ` ( L ` k ) ) ) )
30 29 eqcomd 
 |-  ( ( ph /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( X ` ( L ` j ) ) x. ( X ` ( L ` k ) ) ) = ( X ` ( L ` ( j x. k ) ) ) )
31 25 30 sylan2 
 |-  ( ( ph /\ ( j e. { q e. NN | q || A } /\ k e. { q e. NN | q || B } ) ) -> ( ( X ` ( L ` j ) ) x. ( X ` ( L ` k ) ) ) = ( X ` ( L ` ( j x. k ) ) ) )
32 2fveq3 
 |-  ( i = ( j x. k ) -> ( X ` ( L ` i ) ) = ( X ` ( L ` ( j x. k ) ) ) )
33 9 10 11 12 13 14 19 24 31 32 fsumdvdsmul 
 |-  ( ph -> ( sum_ j e. { q e. NN | q || A } ( X ` ( L ` j ) ) x. sum_ k e. { q e. NN | q || B } ( X ` ( L ` k ) ) ) = sum_ i e. { q e. NN | q || ( A x. B ) } ( X ` ( L ` i ) ) )
34 1 2 3 4 5 6 7 dchrisum0fval 
 |-  ( A e. NN -> ( F ` A ) = sum_ j e. { q e. NN | q || A } ( X ` ( L ` j ) ) )
35 9 34 syl 
 |-  ( ph -> ( F ` A ) = sum_ j e. { q e. NN | q || A } ( X ` ( L ` j ) ) )
36 1 2 3 4 5 6 7 dchrisum0fval 
 |-  ( B e. NN -> ( F ` B ) = sum_ k e. { q e. NN | q || B } ( X ` ( L ` k ) ) )
37 10 36 syl 
 |-  ( ph -> ( F ` B ) = sum_ k e. { q e. NN | q || B } ( X ` ( L ` k ) ) )
38 35 37 oveq12d 
 |-  ( ph -> ( ( F ` A ) x. ( F ` B ) ) = ( sum_ j e. { q e. NN | q || A } ( X ` ( L ` j ) ) x. sum_ k e. { q e. NN | q || B } ( X ` ( L ` k ) ) ) )
39 9 10 nnmulcld 
 |-  ( ph -> ( A x. B ) e. NN )
40 1 2 3 4 5 6 7 dchrisum0fval 
 |-  ( ( A x. B ) e. NN -> ( F ` ( A x. B ) ) = sum_ i e. { q e. NN | q || ( A x. B ) } ( X ` ( L ` i ) ) )
41 39 40 syl 
 |-  ( ph -> ( F ` ( A x. B ) ) = sum_ i e. { q e. NN | q || ( A x. B ) } ( X ` ( L ` i ) ) )
42 33 38 41 3eqtr4rd 
 |-  ( ph -> ( F ` ( A x. B ) ) = ( ( F ` A ) x. ( F ` B ) ) )