Metamath Proof Explorer

Theorem dchrsum

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 )
dchrsum.b 
|- B = ( Base ` Z )
Assertion dchrsum 
|- ( ph -> sum_ a e. B ( 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 dchrsum.b 
 |-  B = ( Base ` Z )
7 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
8 6 7 unitss 
 |-  ( Unit ` Z ) C_ B
9 8 a1i 
 |-  ( ph -> ( Unit ` Z ) C_ B )
10 1 2 3 6 5 dchrf 
 |-  ( ph -> X : B --> CC )
11 8 sseli 
 |-  ( a e. ( Unit ` Z ) -> a e. B )
12 ffvelrn 
 |-  ( ( X : B --> CC /\ a e. B ) -> ( X ` a ) e. CC )
13 10 11 12 syl2an 
 |-  ( ( ph /\ a e. ( Unit ` Z ) ) -> ( X ` a ) e. CC )
14 eldif 
 |-  ( a e. ( B \ ( Unit ` Z ) ) <-> ( a e. B /\ -. a e. ( Unit ` Z ) ) )
15 5 adantr 
 |-  ( ( ph /\ a e. B ) -> X e. D )
16 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
17 1 2 3 6 7 15 16 dchrn0 
 |-  ( ( ph /\ a e. B ) -> ( ( X ` a ) =/= 0 <-> a e. ( Unit ` Z ) ) )
18 17 biimpd 
 |-  ( ( ph /\ a e. B ) -> ( ( X ` a ) =/= 0 -> a e. ( Unit ` Z ) ) )
19 18 necon1bd 
 |-  ( ( ph /\ a e. B ) -> ( -. a e. ( Unit ` Z ) -> ( X ` a ) = 0 ) )
20 19 impr 
 |-  ( ( ph /\ ( a e. B /\ -. a e. ( Unit ` Z ) ) ) -> ( X ` a ) = 0 )
21 14 20 sylan2b 
 |-  ( ( ph /\ a e. ( B \ ( Unit ` Z ) ) ) -> ( X ` a ) = 0 )
22 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
23 2 6 znfi 
 |-  ( N e. NN -> B e. Fin )
24 5 22 23 3syl 
 |-  ( ph -> B e. Fin )
25 9 13 21 24 fsumss 
 |-  ( ph -> sum_ a e. ( Unit ` Z ) ( X ` a ) = sum_ a e. B ( X ` a ) )
26 1 2 3 4 5 7 dchrsum2 
 |-  ( ph -> sum_ a e. ( Unit ` Z ) ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )
27 25 26 eqtr3d 
 |-  ( ph -> sum_ a e. B ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )