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