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