Metamath Proof Explorer

Theorem dchrsum2

Description: An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrsum.g 
|- G = ( DChr ` N )
dchrsum.z 
|- Z = ( Z/nZ ` N )
dchrsum.d 
|- D = ( Base ` G )
dchrsum.1 
|- .1. = ( 0g ` G )
dchrsum.x 
|- ( ph -> X e. D )
dchrsum2.u 
|- U = ( Unit ` Z )
Assertion dchrsum2 
|- ( ph -> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )

Proof

Step Hyp Ref Expression
1 dchrsum.g 
 |-  G = ( DChr ` N )
2 dchrsum.z 
 |-  Z = ( Z/nZ ` N )
3 dchrsum.d 
 |-  D = ( Base ` G )
4 dchrsum.1 
 |-  .1. = ( 0g ` G )
5 dchrsum.x 
 |-  ( ph -> X e. D )
6 dchrsum2.u 
 |-  U = ( Unit ` Z )
7 eqeq2 
 |-  ( ( phi ` N ) = if ( X = .1. , ( phi ` N ) , 0 ) -> ( sum_ a e. U ( X ` a ) = ( phi ` N ) <-> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) ) )
8 eqeq2 
 |-  ( 0 = if ( X = .1. , ( phi ` N ) , 0 ) -> ( sum_ a e. U ( X ` a ) = 0 <-> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) ) )
9 fveq1 
 |-  ( X = .1. -> ( X ` a ) = ( .1. ` a ) )
10 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
11 5 10 syl 
 |-  ( ph -> N e. NN )
12 11 adantr 
 |-  ( ( ph /\ a e. U ) -> N e. NN )
13 simpr 
 |-  ( ( ph /\ a e. U ) -> a e. U )
14 1 2 4 6 12 13 dchr1 
 |-  ( ( ph /\ a e. U ) -> ( .1. ` a ) = 1 )
15 9 14 sylan9eqr 
 |-  ( ( ( ph /\ a e. U ) /\ X = .1. ) -> ( X ` a ) = 1 )
16 15 an32s 
 |-  ( ( ( ph /\ X = .1. ) /\ a e. U ) -> ( X ` a ) = 1 )
17 16 sumeq2dv 
 |-  ( ( ph /\ X = .1. ) -> sum_ a e. U ( X ` a ) = sum_ a e. U 1 )
18 2 6 znunithash 
 |-  ( N e. NN -> ( # ` U ) = ( phi ` N ) )
19 11 18 syl 
 |-  ( ph -> ( # ` U ) = ( phi ` N ) )
20 11 phicld 
 |-  ( ph -> ( phi ` N ) e. NN )
21 20 nnnn0d 
 |-  ( ph -> ( phi ` N ) e. NN0 )
22 19 21 eqeltrd 
 |-  ( ph -> ( # ` U ) e. NN0 )
23 6 fvexi 
 |-  U e. _V
24 hashclb 
 |-  ( U e. _V -> ( U e. Fin <-> ( # ` U ) e. NN0 ) )
25 23 24 ax-mp 
 |-  ( U e. Fin <-> ( # ` U ) e. NN0 )
26 22 25 sylibr 
 |-  ( ph -> U e. Fin )
27 ax-1cn 
 |-  1 e. CC
28 fsumconst 
 |-  ( ( U e. Fin /\ 1 e. CC ) -> sum_ a e. U 1 = ( ( # ` U ) x. 1 ) )
29 26 27 28 sylancl 
 |-  ( ph -> sum_ a e. U 1 = ( ( # ` U ) x. 1 ) )
30 19 oveq1d 
 |-  ( ph -> ( ( # ` U ) x. 1 ) = ( ( phi ` N ) x. 1 ) )
31 20 nncnd 
 |-  ( ph -> ( phi ` N ) e. CC )
32 31 mulid1d 
 |-  ( ph -> ( ( phi ` N ) x. 1 ) = ( phi ` N ) )
33 29 30 32 3eqtrd 
 |-  ( ph -> sum_ a e. U 1 = ( phi ` N ) )
34 33 adantr 
 |-  ( ( ph /\ X = .1. ) -> sum_ a e. U 1 = ( phi ` N ) )
35 17 34 eqtrd 
 |-  ( ( ph /\ X = .1. ) -> sum_ a e. U ( X ` a ) = ( phi ` N ) )
36 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
37 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
38 3 4 grpidcl 
 |-  ( G e. Grp -> .1. e. D )
39 11 36 37 38 4syl 
 |-  ( ph -> .1. e. D )
40 1 2 3 6 5 39 dchreq 
 |-  ( ph -> ( X = .1. <-> A. k e. U ( X ` k ) = ( .1. ` k ) ) )
41 40 notbid 
 |-  ( ph -> ( -. X = .1. <-> -. A. k e. U ( X ` k ) = ( .1. ` k ) ) )
42 rexnal 
 |-  ( E. k e. U -. ( X ` k ) = ( .1. ` k ) <-> -. A. k e. U ( X ` k ) = ( .1. ` k ) )
43 41 42 bitr4di 
 |-  ( ph -> ( -. X = .1. <-> E. k e. U -. ( X ` k ) = ( .1. ` k ) ) )
44 df-ne 
 |-  ( ( X ` k ) =/= ( .1. ` k ) <-> -. ( X ` k ) = ( .1. ` k ) )
45 11 adantr 
 |-  ( ( ph /\ k e. U ) -> N e. NN )
46 simpr 
 |-  ( ( ph /\ k e. U ) -> k e. U )
47 1 2 4 6 45 46 dchr1 
 |-  ( ( ph /\ k e. U ) -> ( .1. ` k ) = 1 )
48 47 neeq2d 
 |-  ( ( ph /\ k e. U ) -> ( ( X ` k ) =/= ( .1. ` k ) <-> ( X ` k ) =/= 1 ) )
49 26 adantr 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> U e. Fin )
50 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
51 1 2 3 50 5 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
52 50 6 unitss 
 |-  U C_ ( Base ` Z )
53 52 sseli 
 |-  ( a e. U -> a e. ( Base ` Z ) )
54 ffvelrn 
 |-  ( ( X : ( Base ` Z ) --> CC /\ a e. ( Base ` Z ) ) -> ( X ` a ) e. CC )
55 51 53 54 syl2an 
 |-  ( ( ph /\ a e. U ) -> ( X ` a ) e. CC )
56 55 adantlr 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ a e. U ) -> ( X ` a ) e. CC )
57 49 56 fsumcl 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> sum_ a e. U ( X ` a ) e. CC )
58 0cnd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> 0 e. CC )
59 51 adantr 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> X : ( Base ` Z ) --> CC )
60 simprl 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> k e. U )
61 52 60 sselid 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> k e. ( Base ` Z ) )
62 59 61 ffvelrnd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( X ` k ) e. CC )
63 subcl 
 |-  ( ( ( X ` k ) e. CC /\ 1 e. CC ) -> ( ( X ` k ) - 1 ) e. CC )
64 62 27 63 sylancl 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( X ` k ) - 1 ) e. CC )
65 simprr 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( X ` k ) =/= 1 )
66 subeq0 
 |-  ( ( ( X ` k ) e. CC /\ 1 e. CC ) -> ( ( ( X ` k ) - 1 ) = 0 <-> ( X ` k ) = 1 ) )
67 62 27 66 sylancl 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) - 1 ) = 0 <-> ( X ` k ) = 1 ) )
68 67 necon3bid 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) - 1 ) =/= 0 <-> ( X ` k ) =/= 1 ) )
69 65 68 mpbird 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( X ` k ) - 1 ) =/= 0 )
70 oveq2 
 |-  ( x = a -> ( k ( .r ` Z ) x ) = ( k ( .r ` Z ) a ) )
71 70 fveq2d 
 |-  ( x = a -> ( X ` ( k ( .r ` Z ) x ) ) = ( X ` ( k ( .r ` Z ) a ) ) )
72 71 cbvsumv 
 |-  sum_ x e. U ( X ` ( k ( .r ` Z ) x ) ) = sum_ a e. U ( X ` ( k ( .r ` Z ) a ) )
73 1 2 3 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
74 73 5 sselid 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
75 74 ad2antrr 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ a e. U ) -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
76 61 adantr 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ a e. U ) -> k e. ( Base ` Z ) )
77 53 adantl 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ a e. U ) -> a e. ( Base ` Z ) )
78 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
79 78 50 mgpbas 
 |-  ( Base ` Z ) = ( Base ` ( mulGrp ` Z ) )
80 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
81 78 80 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
82 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
83 cnfldmul 
 |-  x. = ( .r ` CCfld )
84 82 83 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
85 79 81 84 mhmlin 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ k e. ( Base ` Z ) /\ a e. ( Base ` Z ) ) -> ( X ` ( k ( .r ` Z ) a ) ) = ( ( X ` k ) x. ( X ` a ) ) )
86 75 76 77 85 syl3anc 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ a e. U ) -> ( X ` ( k ( .r ` Z ) a ) ) = ( ( X ` k ) x. ( X ` a ) ) )
87 86 sumeq2dv 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> sum_ a e. U ( X ` ( k ( .r ` Z ) a ) ) = sum_ a e. U ( ( X ` k ) x. ( X ` a ) ) )
88 72 87 eqtrid 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> sum_ x e. U ( X ` ( k ( .r ` Z ) x ) ) = sum_ a e. U ( ( X ` k ) x. ( X ` a ) ) )
89 fveq2 
 |-  ( a = ( k ( .r ` Z ) x ) -> ( X ` a ) = ( X ` ( k ( .r ` Z ) x ) ) )
90 11 nnnn0d 
 |-  ( ph -> N e. NN0 )
91 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
92 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
93 eqid 
 |-  ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U )
94 6 93 unitgrp 
 |-  ( Z e. Ring -> ( ( mulGrp ` Z ) |`s U ) e. Grp )
95 90 91 92 94 4syl 
 |-  ( ph -> ( ( mulGrp ` Z ) |`s U ) e. Grp )
96 eqid 
 |-  ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) ) = ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) )
97 6 93 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` Z ) |`s U ) )
98 93 81 ressplusg 
 |-  ( U e. _V -> ( .r ` Z ) = ( +g ` ( ( mulGrp ` Z ) |`s U ) ) )
99 23 98 ax-mp 
 |-  ( .r ` Z ) = ( +g ` ( ( mulGrp ` Z ) |`s U ) )
100 96 97 99 grplactf1o 
 |-  ( ( ( ( mulGrp ` Z ) |`s U ) e. Grp /\ k e. U ) -> ( ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) ) ` k ) : U -1-1-onto-> U )
101 95 60 100 syl2an2r 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) ) ` k ) : U -1-1-onto-> U )
102 96 97 grplactval 
 |-  ( ( k e. U /\ x e. U ) -> ( ( ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) ) ` k ) ` x ) = ( k ( .r ` Z ) x ) )
103 60 102 sylan 
 |-  ( ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) /\ x e. U ) -> ( ( ( b e. U |-> ( c e. U |-> ( b ( .r ` Z ) c ) ) ) ` k ) ` x ) = ( k ( .r ` Z ) x ) )
104 89 49 101 103 56 fsumf1o 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> sum_ a e. U ( X ` a ) = sum_ x e. U ( X ` ( k ( .r ` Z ) x ) ) )
105 49 62 56 fsummulc2 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( X ` k ) x. sum_ a e. U ( X ` a ) ) = sum_ a e. U ( ( X ` k ) x. ( X ` a ) ) )
106 88 104 105 3eqtr4rd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( X ` k ) x. sum_ a e. U ( X ` a ) ) = sum_ a e. U ( X ` a ) )
107 57 mulid2d 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( 1 x. sum_ a e. U ( X ` a ) ) = sum_ a e. U ( X ` a ) )
108 106 107 oveq12d 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) x. sum_ a e. U ( X ` a ) ) - ( 1 x. sum_ a e. U ( X ` a ) ) ) = ( sum_ a e. U ( X ` a ) - sum_ a e. U ( X ` a ) ) )
109 57 subidd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( sum_ a e. U ( X ` a ) - sum_ a e. U ( X ` a ) ) = 0 )
110 108 109 eqtrd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) x. sum_ a e. U ( X ` a ) ) - ( 1 x. sum_ a e. U ( X ` a ) ) ) = 0 )
111 1cnd 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> 1 e. CC )
112 62 111 57 subdird 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) - 1 ) x. sum_ a e. U ( X ` a ) ) = ( ( ( X ` k ) x. sum_ a e. U ( X ` a ) ) - ( 1 x. sum_ a e. U ( X ` a ) ) ) )
113 64 mul01d 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) - 1 ) x. 0 ) = 0 )
114 110 112 113 3eqtr4d 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> ( ( ( X ` k ) - 1 ) x. sum_ a e. U ( X ` a ) ) = ( ( ( X ` k ) - 1 ) x. 0 ) )
115 57 58 64 69 114 mulcanad 
 |-  ( ( ph /\ ( k e. U /\ ( X ` k ) =/= 1 ) ) -> sum_ a e. U ( X ` a ) = 0 )
116 115 expr 
 |-  ( ( ph /\ k e. U ) -> ( ( X ` k ) =/= 1 -> sum_ a e. U ( X ` a ) = 0 ) )
117 48 116 sylbid 
 |-  ( ( ph /\ k e. U ) -> ( ( X ` k ) =/= ( .1. ` k ) -> sum_ a e. U ( X ` a ) = 0 ) )
118 44 117 syl5bir 
 |-  ( ( ph /\ k e. U ) -> ( -. ( X ` k ) = ( .1. ` k ) -> sum_ a e. U ( X ` a ) = 0 ) )
119 118 rexlimdva 
 |-  ( ph -> ( E. k e. U -. ( X ` k ) = ( .1. ` k ) -> sum_ a e. U ( X ` a ) = 0 ) )
120 43 119 sylbid 
 |-  ( ph -> ( -. X = .1. -> sum_ a e. U ( X ` a ) = 0 ) )
121 120 imp 
 |-  ( ( ph /\ -. X = .1. ) -> sum_ a e. U ( X ` a ) = 0 )
122 7 8 35 121 ifbothda 
 |-  ( ph -> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )