Metamath Proof Explorer

Theorem sum2dchr

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. Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sum2dchr.g ⊢ G = DChr ⁡ N
sum2dchr.d ⊢ D = Base G
sum2dchr.z ⊢ Z = ℤ/Nℤ
sum2dchr.b ⊢ B = Base Z
sum2dchr.u ⊢ U = Unit ⁡ Z
sum2dchr.n ⊢ φ → N ∈ ℕ
sum2dchr.a ⊢ φ → A ∈ B
sum2dchr.c ⊢ φ → C ∈ U
Assertion sum2dchr ⊢ φ → ∑ x ∈ D x ⁡ A ⁢ x ⁡ C ‾ = if A = C ϕ ⁡ N 0

Proof

Step Hyp Ref Expression
1 sum2dchr.g ⊢ G = DChr ⁡ N
2 sum2dchr.d ⊢ D = Base G
3 sum2dchr.z ⊢ Z = ℤ/Nℤ
4 sum2dchr.b ⊢ B = Base Z
5 sum2dchr.u ⊢ U = Unit ⁡ Z
6 sum2dchr.n ⊢ φ → N ∈ ℕ
7 sum2dchr.a ⊢ φ → A ∈ B
8 sum2dchr.c ⊢ φ → C ∈ U
9 eqid ⊢ 1 Z = 1 Z
10 6 nnnn0d ⊢ φ → N ∈ ℕ 0
11 3 zncrng ⊢ N ∈ ℕ 0 → Z ∈ CRing
12 crngring ⊢ Z ∈ CRing → Z ∈ Ring
13 10 11 12 3syl ⊢ φ → Z ∈ Ring
14 eqid ⊢ / r ⁡ Z = / r ⁡ Z
15 4 5 14 dvrcl ⊢ Z ∈ Ring ∧ A ∈ B ∧ C ∈ U → A / r ⁡ Z C ∈ B
16 13 7 8 15 syl3anc ⊢ φ → A / r ⁡ Z C ∈ B
17 1 2 3 9 4 6 16 sumdchr ⊢ φ → ∑ x ∈ D x ⁡ A / r ⁡ Z C = if A / r ⁡ Z C = 1 Z ϕ ⁡ N 0
18 eqid ⊢ ⋅ Z = ⋅ Z
19 eqid ⊢ inv r ⁡ Z = inv r ⁡ Z
20 4 18 5 19 14 dvrval ⊢ A ∈ B ∧ C ∈ U → A / r ⁡ Z C = A ⋅ Z inv r ⁡ Z ⁡ C
21 7 8 20 syl2anc ⊢ φ → A / r ⁡ Z C = A ⋅ Z inv r ⁡ Z ⁡ C
22 21 adantr ⊢ φ ∧ x ∈ D → A / r ⁡ Z C = A ⋅ Z inv r ⁡ Z ⁡ C
23 22 fveq2d ⊢ φ ∧ x ∈ D → x ⁡ A / r ⁡ Z C = x ⁡ A ⋅ Z inv r ⁡ Z ⁡ C
24 1 3 2 dchrmhm ⊢ D ⊆ mulGrp Z MndHom mulGrp ℂ fld
25 simpr ⊢ φ ∧ x ∈ D → x ∈ D
26 24 25 sseldi ⊢ φ ∧ x ∈ D → x ∈ mulGrp Z MndHom mulGrp ℂ fld
27 7 adantr ⊢ φ ∧ x ∈ D → A ∈ B
28 4 5 unitss ⊢ U ⊆ B
29 5 19 unitinvcl ⊢ Z ∈ Ring ∧ C ∈ U → inv r ⁡ Z ⁡ C ∈ U
30 13 8 29 syl2anc ⊢ φ → inv r ⁡ Z ⁡ C ∈ U
31 30 adantr ⊢ φ ∧ x ∈ D → inv r ⁡ Z ⁡ C ∈ U
32 28 31 sseldi ⊢ φ ∧ x ∈ D → inv r ⁡ Z ⁡ C ∈ B
33 eqid ⊢ mulGrp Z = mulGrp Z
34 33 4 mgpbas ⊢ B = Base mulGrp Z
35 33 18 mgpplusg ⊢ ⋅ Z = + mulGrp Z
36 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
37 cnfldmul ⊢ × = ⋅ ℂ fld
38 36 37 mgpplusg ⊢ × = + mulGrp ℂ fld
39 34 35 38 mhmlin ⊢ x ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ A ∈ B ∧ inv r ⁡ Z ⁡ C ∈ B → x ⁡ A ⋅ Z inv r ⁡ Z ⁡ C = x ⁡ A ⁢ x ⁡ inv r ⁡ Z ⁡ C
40 26 27 32 39 syl3anc ⊢ φ ∧ x ∈ D → x ⁡ A ⋅ Z inv r ⁡ Z ⁡ C = x ⁡ A ⁢ x ⁡ inv r ⁡ Z ⁡ C
41 eqid ⊢ mulGrp Z ↾ 𝑠 U = mulGrp Z ↾ 𝑠 U
42 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
43 1 3 2 5 41 42 25 dchrghm ⊢ φ ∧ x ∈ D → x ↾ U ∈ mulGrp Z ↾ 𝑠 U GrpHom mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
44 8 adantr ⊢ φ ∧ x ∈ D → C ∈ U
45 5 41 unitgrpbas ⊢ U = Base mulGrp Z ↾ 𝑠 U
46 5 41 19 invrfval ⊢ inv r ⁡ Z = inv g ⁡ mulGrp Z ↾ 𝑠 U
47 cnfldbas ⊢ ℂ = Base ℂ fld
48 cnfld0 ⊢ 0 = 0 ℂ fld
49 cndrng ⊢ ℂ fld ∈ DivRing
50 47 48 49 drngui ⊢ ℂ ∖ 0 = Unit ⁡ ℂ fld
51 eqid ⊢ inv r ⁡ ℂ fld = inv r ⁡ ℂ fld
52 50 42 51 invrfval ⊢ inv r ⁡ ℂ fld = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
53 45 46 52 ghminv ⊢ x ↾ U ∈ mulGrp Z ↾ 𝑠 U GrpHom mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ∧ C ∈ U → x ↾ U ⁡ inv r ⁡ Z ⁡ C = inv r ⁡ ℂ fld ⁡ x ↾ U ⁡ C
54 43 44 53 syl2anc ⊢ φ ∧ x ∈ D → x ↾ U ⁡ inv r ⁡ Z ⁡ C = inv r ⁡ ℂ fld ⁡ x ↾ U ⁡ C
55 31 fvresd ⊢ φ ∧ x ∈ D → x ↾ U ⁡ inv r ⁡ Z ⁡ C = x ⁡ inv r ⁡ Z ⁡ C
56 44 fvresd ⊢ φ ∧ x ∈ D → x ↾ U ⁡ C = x ⁡ C
57 56 fveq2d ⊢ φ ∧ x ∈ D → inv r ⁡ ℂ fld ⁡ x ↾ U ⁡ C = inv r ⁡ ℂ fld ⁡ x ⁡ C
58 1 3 2 4 25 dchrf ⊢ φ ∧ x ∈ D → x : B ⟶ ℂ
59 28 44 sseldi ⊢ φ ∧ x ∈ D → C ∈ B
60 58 59 ffvelrnd ⊢ φ ∧ x ∈ D → x ⁡ C ∈ ℂ
61 1 3 2 4 5 25 59 dchrn0 ⊢ φ ∧ x ∈ D → x ⁡ C ≠ 0 ↔ C ∈ U
62 44 61 mpbird ⊢ φ ∧ x ∈ D → x ⁡ C ≠ 0
63 cnfldinv ⊢ x ⁡ C ∈ ℂ ∧ x ⁡ C ≠ 0 → inv r ⁡ ℂ fld ⁡ x ⁡ C = 1 x ⁡ C
64 60 62 63 syl2anc ⊢ φ ∧ x ∈ D → inv r ⁡ ℂ fld ⁡ x ⁡ C = 1 x ⁡ C
65 recval ⊢ x ⁡ C ∈ ℂ ∧ x ⁡ C ≠ 0 → 1 x ⁡ C = x ⁡ C ‾ x ⁡ C 2
66 60 62 65 syl2anc ⊢ φ ∧ x ∈ D → 1 x ⁡ C = x ⁡ C ‾ x ⁡ C 2
67 1 2 25 3 5 44 dchrabs ⊢ φ ∧ x ∈ D → x ⁡ C = 1
68 67 oveq1d ⊢ φ ∧ x ∈ D → x ⁡ C 2 = 1 2
69 sq1 ⊢ 1 2 = 1
70 68 69 eqtrdi ⊢ φ ∧ x ∈ D → x ⁡ C 2 = 1
71 70 oveq2d ⊢ φ ∧ x ∈ D → x ⁡ C ‾ x ⁡ C 2 = x ⁡ C ‾ 1
72 60 cjcld ⊢ φ ∧ x ∈ D → x ⁡ C ‾ ∈ ℂ
73 72 div1d ⊢ φ ∧ x ∈ D → x ⁡ C ‾ 1 = x ⁡ C ‾
74 66 71 73 3eqtrd ⊢ φ ∧ x ∈ D → 1 x ⁡ C = x ⁡ C ‾
75 57 64 74 3eqtrd ⊢ φ ∧ x ∈ D → inv r ⁡ ℂ fld ⁡ x ↾ U ⁡ C = x ⁡ C ‾
76 54 55 75 3eqtr3d ⊢ φ ∧ x ∈ D → x ⁡ inv r ⁡ Z ⁡ C = x ⁡ C ‾
77 76 oveq2d ⊢ φ ∧ x ∈ D → x ⁡ A ⁢ x ⁡ inv r ⁡ Z ⁡ C = x ⁡ A ⁢ x ⁡ C ‾
78 23 40 77 3eqtrd ⊢ φ ∧ x ∈ D → x ⁡ A / r ⁡ Z C = x ⁡ A ⁢ x ⁡ C ‾
79 78 sumeq2dv ⊢ φ → ∑ x ∈ D x ⁡ A / r ⁡ Z C = ∑ x ∈ D x ⁡ A ⁢ x ⁡ C ‾
80 4 5 14 9 dvreq1 ⊢ Z ∈ Ring ∧ A ∈ B ∧ C ∈ U → A / r ⁡ Z C = 1 Z ↔ A = C
81 13 7 8 80 syl3anc ⊢ φ → A / r ⁡ Z C = 1 Z ↔ A = C
82 81 ifbid ⊢ φ → if A / r ⁡ Z C = 1 Z ϕ ⁡ N 0 = if A = C ϕ ⁡ N 0
83 17 79 82 3eqtr3d ⊢ φ → ∑ x ∈ D x ⁡ A ⁢ x ⁡ C ‾ = if A = C ϕ ⁡ N 0