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

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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
sum2dchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
sum2dchr.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
sum2dchr.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
sum2dchr.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
sum2dchr.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
sum2dchr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
sum2dchr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion sum2dchr ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 sum2dchr.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 sum2dchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 sum2dchr.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
4 sum2dchr.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 sum2dchr.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
6 sum2dchr.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 sum2dchr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8 sum2dchr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
9 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
10 6 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 3 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
12 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
13 10 11 12 3syl ⊢ ( 𝜑 → 𝑍 ∈ Ring )
14 eqid ⊢ ( /r ‘ 𝑍 ) = ( /r ‘ 𝑍 )
15 4 5 14 dvrcl ⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 )
16 13 7 8 15 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 )
17 1 2 3 9 4 6 16 sumdchr ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
18 eqid ⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
19 eqid ⊢ ( invr ‘ 𝑍 ) = ( invr ‘ 𝑍 )
20 4 18 5 19 14 dvrval ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
21 7 8 20 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
24 1 3 2 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
26 24 25 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
27 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐵 )
28 4 5 unitss ⊢ 𝑈 ⊆ 𝐵
29 5 19 unitinvcl ⊢ ( ( 𝑍 ∈ Ring ∧ 𝐶 ∈ 𝑈 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
30 13 8 29 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
32 28 31 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 )
33 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
34 33 4 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
35 33 18 mgpplusg ⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
36 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
37 cnfldmul ⊢ · = ( .r ‘ ℂfld )
38 36 37 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
39 34 35 38 mhmlin ⊢ ( ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝐴 ∈ 𝐵 ∧ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
40 26 27 32 39 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
41 eqid ⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
42 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
43 1 3 2 5 41 42 25 dchrghm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) )
44 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝑈 )
45 5 41 unitgrpbas ⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
46 5 41 19 invrfval ⊢ ( invr ‘ 𝑍 ) = ( invg ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
47 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
48 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
49 cndrng ⊢ ℂfld ∈ DivRing
50 47 48 49 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
51 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
52 50 42 51 invrfval ⊢ ( invr ‘ ℂfld ) = ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
53 45 46 52 ghminv ⊢ ( ( ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) )
54 43 44 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) )
55 31 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
56 44 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) = ( 𝑥 ‘ 𝐶 ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) )
58 1 3 2 4 25 dchrf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐵 ⟶ ℂ )
59 28 44 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝐵 )
60 58 59 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ∈ ℂ )
61 1 3 2 4 5 25 59 dchrn0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐶 ) ≠ 0 ↔ 𝐶 ∈ 𝑈 ) )
62 44 61 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ≠ 0 )
63 cnfldinv ⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) )
64 60 62 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) )
65 recval ⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) )
66 60 62 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) )
67 1 2 25 3 5 44 dchrabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) = 1 )
68 67 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
69 sq1 ⊢ ( 1 ↑ 2 ) = 1
70 68 69 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = 1 )
71 70 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) )
72 60 cjcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ∈ ℂ )
73 72 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
74 66 71 73 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
75 57 64 74 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
76 54 55 75 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
77 76 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
78 23 40 77 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
79 78 sumeq2dv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
80 4 5 14 9 dvreq1 ⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) )
81 13 7 8 80 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) )
82 81 ifbid ⊢ ( 𝜑 → if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )
83 17 79 82 3eqtr3d ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )