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 𝐺 = ( DChr ‘ 𝑁 )
sumdchr.d 𝐷 = ( Base ‘ 𝐺 )
sumdchr.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
sumdchr.1 1 = ( 1r𝑍 )
sumdchr.b 𝐵 = ( Base ‘ 𝑍 )
sumdchr.n ( 𝜑𝑁 ∈ ℕ )
sumdchr.a ( 𝜑𝐴𝐵 )
Assertion sumdchr ( 𝜑 → Σ 𝑥𝐷 ( 𝑥𝐴 ) = if ( 𝐴 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

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