Theorem dchrsum

Description: An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrsum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrsum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrsum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrsum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrsum.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrsum.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
Assertion	dchrsum	⊢ ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		dchrsum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrsum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrsum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrsum.1	⊢ 1 = ( 0g ‘ 𝐺 )
5		dchrsum.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6		dchrsum.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
7		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
8	6 7	unitss	⊢ ( Unit ‘ 𝑍 ) ⊆ 𝐵
9	8	a1i	⊢ ( 𝜑 → ( Unit ‘ 𝑍 ) ⊆ 𝐵 )
10	1 2 3 6 5	dchrf	⊢ ( 𝜑 → 𝑋 : 𝐵 ⟶ ℂ )
11	8	sseli	⊢ ( 𝑎 ∈ ( Unit ‘ 𝑍 ) → 𝑎 ∈ 𝐵 )
12		ffvelrn	⊢ ( ( 𝑋 : 𝐵 ⟶ ℂ ∧ 𝑎 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
13	10 11 12	syl2an	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Unit ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
14		eldif	⊢ ( 𝑎 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑍 ) ) ↔ ( 𝑎 ∈ 𝐵 ∧ ¬ 𝑎 ∈ ( Unit ‘ 𝑍 ) ) )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐷 )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
17	1 2 3 6 7 15 16	dchrn0	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑎 ) ≠ 0 ↔ 𝑎 ∈ ( Unit ‘ 𝑍 ) ) )
18	17	biimpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑎 ) ≠ 0 → 𝑎 ∈ ( Unit ‘ 𝑍 ) ) )
19	18	necon1bd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ¬ 𝑎 ∈ ( Unit ‘ 𝑍 ) → ( 𝑋 ‘ 𝑎 ) = 0 ) )
20	19	impr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ ¬ 𝑎 ∈ ( Unit ‘ 𝑍 ) ) ) → ( 𝑋 ‘ 𝑎 ) = 0 )
21	14 20	sylan2b	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑍 ) ) ) → ( 𝑋 ‘ 𝑎 ) = 0 )
22	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
23	2 6	znfi	⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )
24	5 22 23	3syl	⊢ ( 𝜑 → 𝐵 ∈ Fin )
25	9 13 21 24	fsumss	⊢ ( 𝜑 → Σ 𝑎 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ 𝑎 ) = Σ 𝑎 ∈ 𝐵 ( 𝑋 ‘ 𝑎 ) )
26	1 2 3 4 5 7	dchrsum2	⊢ ( 𝜑 → Σ 𝑎 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )
27	25 26	eqtr3d	⊢ ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )