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 ffvelrnd ( ( 𝜑𝑥𝐷 ) → ( 𝑥𝐶 ) ∈ ℂ )
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 ) )