This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ G = DChr ⁡ N
dchrsum.z ⊢ Z = ℤ/Nℤ
dchrsum.d ⊢ D = Base G
dchrsum.1 ⊢ 1 ˙ = 0 G
dchrsum.x ⊢ φ → X ∈ D
dchrsum.b ⊢ B = Base Z
Assertion dchrsum ⊢ φ → ∑ a ∈ B X ⁡ a = if X = 1 ˙ ϕ ⁡ N 0

Proof

Step Hyp Ref Expression
1 dchrsum.g ⊢ G = DChr ⁡ N
2 dchrsum.z ⊢ Z = ℤ/Nℤ
3 dchrsum.d ⊢ D = Base G
4 dchrsum.1 ⊢ 1 ˙ = 0 G
5 dchrsum.x ⊢ φ → X ∈ D
6 dchrsum.b ⊢ B = Base Z
7 eqid ⊢ Unit ⁡ Z = Unit ⁡ Z
8 6 7 unitss ⊢ Unit ⁡ Z ⊆ B
9 8 a1i ⊢ φ → Unit ⁡ Z ⊆ B
10 1 2 3 6 5 dchrf ⊢ φ → X : B ⟶ ℂ
11 8 sseli ⊢ a ∈ Unit ⁡ Z → a ∈ B
12 ffvelcdm ⊢ X : B ⟶ ℂ ∧ a ∈ B → X ⁡ a ∈ ℂ
13 10 11 12 syl2an ⊢ φ ∧ a ∈ Unit ⁡ Z → X ⁡ a ∈ ℂ
14 eldif ⊢ a ∈ B ∖ Unit ⁡ Z ↔ a ∈ B ∧ ¬ a ∈ Unit ⁡ Z
15 5 adantr ⊢ φ ∧ a ∈ B → X ∈ D
16 simpr ⊢ φ ∧ a ∈ B → a ∈ B
17 1 2 3 6 7 15 16 dchrn0 ⊢ φ ∧ a ∈ B → X ⁡ a ≠ 0 ↔ a ∈ Unit ⁡ Z
18 17 biimpd ⊢ φ ∧ a ∈ B → X ⁡ a ≠ 0 → a ∈ Unit ⁡ Z
19 18 necon1bd ⊢ φ ∧ a ∈ B → ¬ a ∈ Unit ⁡ Z → X ⁡ a = 0
20 19 impr ⊢ φ ∧ a ∈ B ∧ ¬ a ∈ Unit ⁡ Z → X ⁡ a = 0
21 14 20 sylan2b ⊢ φ ∧ a ∈ B ∖ Unit ⁡ Z → X ⁡ a = 0
22 1 3 dchrrcl ⊢ X ∈ D → N ∈ ℕ
23 2 6 znfi ⊢ N ∈ ℕ → B ∈ Fin
24 5 22 23 3syl ⊢ φ → B ∈ Fin
25 9 13 21 24 fsumss ⊢ φ → ∑ a ∈ Unit ⁡ Z X ⁡ a = ∑ a ∈ B X ⁡ a
26 1 2 3 4 5 7 dchrsum2 ⊢ φ → ∑ a ∈ Unit ⁡ Z X ⁡ a = if X = 1 ˙ ϕ ⁡ N 0
27 25 26 eqtr3d ⊢ φ → ∑ a ∈ B X ⁡ a = if X = 1 ˙ ϕ ⁡ N 0