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