This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchr2sum

Description: An orthogonality relation for Dirichlet characters: the sum of X ( a ) x. * Y ( a ) over all a is nonzero only when X = Y . Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchr2sum.g 
|- G = ( DChr ` N )
dchr2sum.z 
|- Z = ( Z/nZ ` N )
dchr2sum.d 
|- D = ( Base ` G )
dchr2sum.b 
|- B = ( Base ` Z )
dchr2sum.x 
|- ( ph -> X e. D )
dchr2sum.y 
|- ( ph -> Y e. D )
Assertion dchr2sum 
|- ( ph -> sum_ a e. B ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) = if ( X = Y , ( phi ` N ) , 0 ) )

Proof

Step Hyp Ref Expression
1 dchr2sum.g 
 |-  G = ( DChr ` N )
2 dchr2sum.z 
 |-  Z = ( Z/nZ ` N )
3 dchr2sum.d 
 |-  D = ( Base ` G )
4 dchr2sum.b 
 |-  B = ( Base ` Z )
5 dchr2sum.x 
 |-  ( ph -> X e. D )
6 dchr2sum.y 
 |-  ( ph -> Y e. D )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
9 5 8 syl 
 |-  ( ph -> N e. NN )
10 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
11 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
12 9 10 11 3syl 
 |-  ( ph -> G e. Grp )
13 eqid 
 |-  ( -g ` G ) = ( -g ` G )
14 3 13 grpsubcl 
 |-  ( ( G e. Grp /\ X e. D /\ Y e. D ) -> ( X ( -g ` G ) Y ) e. D )
15 12 5 6 14 syl3anc 
 |-  ( ph -> ( X ( -g ` G ) Y ) e. D )
16 1 2 3 7 15 4 dchrsum 
 |-  ( ph -> sum_ a e. B ( ( X ( -g ` G ) Y ) ` a ) = if ( ( X ( -g ` G ) Y ) = ( 0g ` G ) , ( phi ` N ) , 0 ) )
17 5 adantr 
 |-  ( ( ph /\ a e. B ) -> X e. D )
18 6 adantr 
 |-  ( ( ph /\ a e. B ) -> Y e. D )
19 eqid 
 |-  ( +g ` G ) = ( +g ` G )
20 eqid 
 |-  ( invg ` G ) = ( invg ` G )
21 3 19 20 13 grpsubval 
 |-  ( ( X e. D /\ Y e. D ) -> ( X ( -g ` G ) Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
22 17 18 21 syl2anc 
 |-  ( ( ph /\ a e. B ) -> ( X ( -g ` G ) Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
23 9 adantr 
 |-  ( ( ph /\ a e. B ) -> N e. NN )
24 23 10 11 3syl 
 |-  ( ( ph /\ a e. B ) -> G e. Grp )
25 3 20 grpinvcl 
 |-  ( ( G e. Grp /\ Y e. D ) -> ( ( invg ` G ) ` Y ) e. D )
26 24 18 25 syl2anc 
 |-  ( ( ph /\ a e. B ) -> ( ( invg ` G ) ` Y ) e. D )
27 1 2 3 19 17 26 dchrmul 
 |-  ( ( ph /\ a e. B ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) = ( X oF x. ( ( invg ` G ) ` Y ) ) )
28 22 27 eqtrd 
 |-  ( ( ph /\ a e. B ) -> ( X ( -g ` G ) Y ) = ( X oF x. ( ( invg ` G ) ` Y ) ) )
29 28 fveq1d 
 |-  ( ( ph /\ a e. B ) -> ( ( X ( -g ` G ) Y ) ` a ) = ( ( X oF x. ( ( invg ` G ) ` Y ) ) ` a ) )
30 1 2 3 4 17 dchrf 
 |-  ( ( ph /\ a e. B ) -> X : B --> CC )
31 30 ffnd 
 |-  ( ( ph /\ a e. B ) -> X Fn B )
32 1 2 3 4 26 dchrf 
 |-  ( ( ph /\ a e. B ) -> ( ( invg ` G ) ` Y ) : B --> CC )
33 32 ffnd 
 |-  ( ( ph /\ a e. B ) -> ( ( invg ` G ) ` Y ) Fn B )
34 4 fvexi 
 |-  B e. _V
35 34 a1i 
 |-  ( ( ph /\ a e. B ) -> B e. _V )
36 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
37 fnfvof 
 |-  ( ( ( X Fn B /\ ( ( invg ` G ) ` Y ) Fn B ) /\ ( B e. _V /\ a e. B ) ) -> ( ( X oF x. ( ( invg ` G ) ` Y ) ) ` a ) = ( ( X ` a ) x. ( ( ( invg ` G ) ` Y ) ` a ) ) )
38 31 33 35 36 37 syl22anc 
 |-  ( ( ph /\ a e. B ) -> ( ( X oF x. ( ( invg ` G ) ` Y ) ) ` a ) = ( ( X ` a ) x. ( ( ( invg ` G ) ` Y ) ` a ) ) )
39 1 3 18 20 dchrinv 
 |-  ( ( ph /\ a e. B ) -> ( ( invg ` G ) ` Y ) = ( * o. Y ) )
40 39 fveq1d 
 |-  ( ( ph /\ a e. B ) -> ( ( ( invg ` G ) ` Y ) ` a ) = ( ( * o. Y ) ` a ) )
41 1 2 3 4 18 dchrf 
 |-  ( ( ph /\ a e. B ) -> Y : B --> CC )
42 fvco3 
 |-  ( ( Y : B --> CC /\ a e. B ) -> ( ( * o. Y ) ` a ) = ( * ` ( Y ` a ) ) )
43 41 36 42 syl2anc 
 |-  ( ( ph /\ a e. B ) -> ( ( * o. Y ) ` a ) = ( * ` ( Y ` a ) ) )
44 40 43 eqtrd 
 |-  ( ( ph /\ a e. B ) -> ( ( ( invg ` G ) ` Y ) ` a ) = ( * ` ( Y ` a ) ) )
45 44 oveq2d 
 |-  ( ( ph /\ a e. B ) -> ( ( X ` a ) x. ( ( ( invg ` G ) ` Y ) ` a ) ) = ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) )
46 29 38 45 3eqtrd 
 |-  ( ( ph /\ a e. B ) -> ( ( X ( -g ` G ) Y ) ` a ) = ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) )
47 46 sumeq2dv 
 |-  ( ph -> sum_ a e. B ( ( X ( -g ` G ) Y ) ` a ) = sum_ a e. B ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) )
48 3 7 13 grpsubeq0 
 |-  ( ( G e. Grp /\ X e. D /\ Y e. D ) -> ( ( X ( -g ` G ) Y ) = ( 0g ` G ) <-> X = Y ) )
49 12 5 6 48 syl3anc 
 |-  ( ph -> ( ( X ( -g ` G ) Y ) = ( 0g ` G ) <-> X = Y ) )
50 49 ifbid 
 |-  ( ph -> if ( ( X ( -g ` G ) Y ) = ( 0g ` G ) , ( phi ` N ) , 0 ) = if ( X = Y , ( phi ` N ) , 0 ) )
51 16 47 50 3eqtr3d 
 |-  ( ph -> sum_ a e. B ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) = if ( X = Y , ( phi ` N ) , 0 ) )