Metamath Proof Explorer

Theorem sum2dchr

Description: An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sum2dchr.g 
|- G = ( DChr ` N )
sum2dchr.d 
|- D = ( Base ` G )
sum2dchr.z 
|- Z = ( Z/nZ ` N )
sum2dchr.b 
|- B = ( Base ` Z )
sum2dchr.u 
|- U = ( Unit ` Z )
sum2dchr.n 
|- ( ph -> N e. NN )
sum2dchr.a 
|- ( ph -> A e. B )
sum2dchr.c 
|- ( ph -> C e. U )
Assertion sum2dchr 
|- ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )

Proof

Step Hyp Ref Expression
1 sum2dchr.g 
 |-  G = ( DChr ` N )
2 sum2dchr.d 
 |-  D = ( Base ` G )
3 sum2dchr.z 
 |-  Z = ( Z/nZ ` N )
4 sum2dchr.b 
 |-  B = ( Base ` Z )
5 sum2dchr.u 
 |-  U = ( Unit ` Z )
6 sum2dchr.n 
 |-  ( ph -> N e. NN )
7 sum2dchr.a 
 |-  ( ph -> A e. B )
8 sum2dchr.c 
 |-  ( ph -> C e. U )
9 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
10 6 nnnn0d 
 |-  ( ph -> N e. NN0 )
11 3 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
12 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
13 10 11 12 3syl 
 |-  ( ph -> Z e. Ring )
14 eqid 
 |-  ( /r ` Z ) = ( /r ` Z )
15 4 5 14 dvrcl 
 |-  ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) e. B )
16 13 7 8 15 syl3anc 
 |-  ( ph -> ( A ( /r ` Z ) C ) e. B )
17 1 2 3 9 4 6 16 sumdchr 
 |-  ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) )
18 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
19 eqid 
 |-  ( invr ` Z ) = ( invr ` Z )
20 4 18 5 19 14 dvrval 
 |-  ( ( A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
21 7 8 20 syl2anc 
 |-  ( ph -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
22 21 adantr 
 |-  ( ( ph /\ x e. D ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
23 22 fveq2d 
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) )
24 1 3 2 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
25 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
26 24 25 sseldi 
 |-  ( ( ph /\ x e. D ) -> x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
27 7 adantr 
 |-  ( ( ph /\ x e. D ) -> A e. B )
28 4 5 unitss 
 |-  U C_ B
29 5 19 unitinvcl 
 |-  ( ( Z e. Ring /\ C e. U ) -> ( ( invr ` Z ) ` C ) e. U )
30 13 8 29 syl2anc 
 |-  ( ph -> ( ( invr ` Z ) ` C ) e. U )
31 30 adantr 
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. U )
32 28 31 sseldi 
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. B )
33 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
34 33 4 mgpbas 
 |-  B = ( Base ` ( mulGrp ` Z ) )
35 33 18 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
36 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
37 cnfldmul 
 |-  x. = ( .r ` CCfld )
38 36 37 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
39 34 35 38 mhmlin 
 |-  ( ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A e. B /\ ( ( invr ` Z ) ` C ) e. B ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) )
40 26 27 32 39 syl3anc 
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) )
41 eqid 
 |-  ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U )
42 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
43 1 3 2 5 41 42 25 dchrghm 
 |-  ( ( ph /\ x e. D ) -> ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
44 8 adantr 
 |-  ( ( ph /\ x e. D ) -> C e. U )
45 5 41 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` Z ) |`s U ) )
46 5 41 19 invrfval 
 |-  ( invr ` Z ) = ( invg ` ( ( mulGrp ` Z ) |`s U ) )
47 cnfldbas 
 |-  CC = ( Base ` CCfld )
48 cnfld0 
 |-  0 = ( 0g ` CCfld )
49 cndrng 
 |-  CCfld e. DivRing
50 47 48 49 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
51 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
52 50 42 51 invrfval 
 |-  ( invr ` CCfld ) = ( invg ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
53 45 46 52 ghminv 
 |-  ( ( ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ C e. U ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) )
54 43 44 53 syl2anc 
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) )
55 31 fvresd 
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( x ` ( ( invr ` Z ) ` C ) ) )
56 44 fvresd 
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` C ) = ( x ` C ) )
57 56 fveq2d 
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( ( invr ` CCfld ) ` ( x ` C ) ) )
58 1 3 2 4 25 dchrf 
 |-  ( ( ph /\ x e. D ) -> x : B --> CC )
59 28 44 sseldi 
 |-  ( ( ph /\ x e. D ) -> C e. B )
60 58 59 ffvelrnd 
 |-  ( ( ph /\ x e. D ) -> ( x ` C ) e. CC )
61 1 3 2 4 5 25 59 dchrn0 
 |-  ( ( ph /\ x e. D ) -> ( ( x ` C ) =/= 0 <-> C e. U ) )
62 44 61 mpbird 
 |-  ( ( ph /\ x e. D ) -> ( x ` C ) =/= 0 )
63 cnfldinv 
 |-  ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) )
64 60 62 63 syl2anc 
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) )
65 recval 
 |-  ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) )
66 60 62 65 syl2anc 
 |-  ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) )
67 1 2 25 3 5 44 dchrabs 
 |-  ( ( ph /\ x e. D ) -> ( abs ` ( x ` C ) ) = 1 )
68 67 oveq1d 
 |-  ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = ( 1 ^ 2 ) )
69 sq1 
 |-  ( 1 ^ 2 ) = 1
70 68 69 eqtrdi 
 |-  ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = 1 )
71 70 oveq2d 
 |-  ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) = ( ( * ` ( x ` C ) ) / 1 ) )
72 60 cjcld 
 |-  ( ( ph /\ x e. D ) -> ( * ` ( x ` C ) ) e. CC )
73 72 div1d 
 |-  ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / 1 ) = ( * ` ( x ` C ) ) )
74 66 71 73 3eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( * ` ( x ` C ) ) )
75 57 64 74 3eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( * ` ( x ` C ) ) )
76 54 55 75 3eqtr3d 
 |-  ( ( ph /\ x e. D ) -> ( x ` ( ( invr ` Z ) ` C ) ) = ( * ` ( x ` C ) ) )
77 76 oveq2d 
 |-  ( ( ph /\ x e. D ) -> ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
78 23 40 77 3eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
79 78 sumeq2dv 
 |-  ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
80 4 5 14 9 dvreq1 
 |-  ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) )
81 13 7 8 80 syl3anc 
 |-  ( ph -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) )
82 81 ifbid 
 |-  ( ph -> if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) = if ( A = C , ( phi ` N ) , 0 ) )
83 17 79 82 3eqtr3d 
 |-  ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )