Metamath Proof Explorer


Theorem sumdchr

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. Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sumdchr.g
|- G = ( DChr ` N )
sumdchr.d
|- D = ( Base ` G )
sumdchr.z
|- Z = ( Z/nZ ` N )
sumdchr.1
|- .1. = ( 1r ` Z )
sumdchr.b
|- B = ( Base ` Z )
sumdchr.n
|- ( ph -> N e. NN )
sumdchr.a
|- ( ph -> A e. B )
Assertion sumdchr
|- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( phi ` N ) , 0 ) )

Proof

Step Hyp Ref Expression
1 sumdchr.g
 |-  G = ( DChr ` N )
2 sumdchr.d
 |-  D = ( Base ` G )
3 sumdchr.z
 |-  Z = ( Z/nZ ` N )
4 sumdchr.1
 |-  .1. = ( 1r ` Z )
5 sumdchr.b
 |-  B = ( Base ` Z )
6 sumdchr.n
 |-  ( ph -> N e. NN )
7 sumdchr.a
 |-  ( ph -> A e. B )
8 1 2 3 4 5 6 7 sumdchr2
 |-  ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) )
9 1 2 dchrhash
 |-  ( N e. NN -> ( # ` D ) = ( phi ` N ) )
10 6 9 syl
 |-  ( ph -> ( # ` D ) = ( phi ` N ) )
11 10 ifeq1d
 |-  ( ph -> if ( A = .1. , ( # ` D ) , 0 ) = if ( A = .1. , ( phi ` N ) , 0 ) )
12 8 11 eqtrd
 |-  ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( phi ` N ) , 0 ) )