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 | ⊢ 𝐺 = ( DChr ‘ 𝑁 ) | |
sumdchr.d | ⊢ 𝐷 = ( Base ‘ 𝐺 ) | ||
sumdchr.z | ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) | ||
sumdchr.1 | ⊢ 1 = ( 1r ‘ 𝑍 ) | ||
sumdchr.b | ⊢ 𝐵 = ( Base ‘ 𝑍 ) | ||
sumdchr.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ ) | ||
sumdchr.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) | ||
Assertion | sumdchr | ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumdchr.g | ⊢ 𝐺 = ( DChr ‘ 𝑁 ) | |
2 | sumdchr.d | ⊢ 𝐷 = ( Base ‘ 𝐺 ) | |
3 | sumdchr.z | ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) | |
4 | sumdchr.1 | ⊢ 1 = ( 1r ‘ 𝑍 ) | |
5 | sumdchr.b | ⊢ 𝐵 = ( Base ‘ 𝑍 ) | |
6 | sumdchr.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ ) | |
7 | sumdchr.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) | |
8 | 1 2 3 4 5 6 7 | sumdchr2 | ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) ) |
9 | 1 2 | dchrhash | ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐷 ) = ( ϕ ‘ 𝑁 ) ) |
10 | 6 9 | syl | ⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) = ( ϕ ‘ 𝑁 ) ) |
11 | 10 | ifeq1d | ⊢ ( 𝜑 → if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) = if ( 𝐴 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) ) |
12 | 8 11 | eqtrd | ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) ) |