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 ) ) |
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 ) ) |