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

Metamath Proof Explorer

Theorem dchr2sum

Description: An orthogonality relation for Dirichlet characters: the sum of X ( a ) x. * Y ( a ) over all a is nonzero only when X = Y . Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchr2sum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchr2sum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchr2sum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchr2sum.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchr2sum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchr2sum.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion dchr2sum ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( ( 𝑋 ‘ 𝑎 ) · ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) ) = if ( 𝑋 = 𝑌 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 dchr2sum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchr2sum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchr2sum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchr2sum.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchr2sum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 dchr2sum.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
9 5 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10 1 dchrabl ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
11 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
12 9 10 11 3syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
13 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
14 3 13 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ∈ 𝐷 )
15 12 5 6 14 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ∈ 𝐷 )
16 1 2 3 7 15 4 dchrsum ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ‘ 𝑎 ) = if ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 0g ‘ 𝐺 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐷 )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑌 ∈ 𝐷 )
19 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
20 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
21 3 19 20 13 grpsubval ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
22 17 18 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑁 ∈ ℕ )
24 23 10 11 3syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐺 ∈ Grp )
25 3 20 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐷 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐷 )
26 24 18 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐷 )
27 1 2 3 19 17 26 dchrmul ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = ( 𝑋 ∘f · ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
28 22 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ∘f · ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
29 28 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ‘ 𝑎 ) = ( ( 𝑋 ∘f · ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑎 ) )
30 1 2 3 4 17 dchrf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 : 𝐵 ⟶ ℂ )
31 30 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 Fn 𝐵 )
32 1 2 3 4 26 dchrf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) : 𝐵 ⟶ ℂ )
33 32 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) Fn 𝐵 )
34 4 fvexi ⊢ 𝐵 ∈ V
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 ∈ V )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
37 fnfvof ⊢ ( ( ( 𝑋 Fn 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) Fn 𝐵 ) ∧ ( 𝐵 ∈ V ∧ 𝑎 ∈ 𝐵 ) ) → ( ( 𝑋 ∘f · ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑎 ) = ( ( 𝑋 ‘ 𝑎 ) · ( ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑎 ) ) )
38 31 33 35 36 37 syl22anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ∘f · ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑎 ) = ( ( 𝑋 ‘ 𝑎 ) · ( ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑎 ) ) )
39 1 3 18 20 dchrinv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) = ( ∗ ∘ 𝑌 ) )
40 39 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑎 ) = ( ( ∗ ∘ 𝑌 ) ‘ 𝑎 ) )
41 1 2 3 4 18 dchrf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑌 : 𝐵 ⟶ ℂ )
42 fvco3 ⊢ ( ( 𝑌 : 𝐵 ⟶ ℂ ∧ 𝑎 ∈ 𝐵 ) → ( ( ∗ ∘ 𝑌 ) ‘ 𝑎 ) = ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) )
43 41 36 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∗ ∘ 𝑌 ) ‘ 𝑎 ) = ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) )
44 40 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑎 ) = ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑎 ) · ( ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑎 ) ) = ( ( 𝑋 ‘ 𝑎 ) · ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) ) )
46 29 38 45 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ‘ 𝑎 ) = ( ( 𝑋 ‘ 𝑎 ) · ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) ) )
47 46 sumeq2dv ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) ‘ 𝑎 ) = Σ 𝑎 ∈ 𝐵 ( ( 𝑋 ‘ 𝑎 ) · ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) ) )
48 3 7 13 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 0g ‘ 𝐺 ) ↔ 𝑋 = 𝑌 ) )
49 12 5 6 48 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 0g ‘ 𝐺 ) ↔ 𝑋 = 𝑌 ) )
50 49 ifbid ⊢ ( 𝜑 → if ( ( 𝑋 ( -g ‘ 𝐺 ) 𝑌 ) = ( 0g ‘ 𝐺 ) , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝑋 = 𝑌 , ( ϕ ‘ 𝑁 ) , 0 ) )
51 16 47 50 3eqtr3d ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝐵 ( ( 𝑋 ‘ 𝑎 ) · ( ∗ ‘ ( 𝑌 ‘ 𝑎 ) ) ) = if ( 𝑋 = 𝑌 , ( ϕ ‘ 𝑁 ) , 0 ) )