Metamath Proof Explorer

Theorem dchrhash

Description: There are exactly phi ( N ) Dirichlet characters modulo N . Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sumdchr.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
sumdchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion dchrhash ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐷 ) = ( ϕ ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 sumdchr.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 sumdchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
4 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
5 3 4 znfi ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin )
6 1 2 dchrfi ⊢ ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )
7 simprr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
8 1 3 2 4 7 dchrf ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝐷 ) ) → 𝑥 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
9 simprl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝐷 ) ) → 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
10 8 9 ffvelcdmd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝐷 ) ) → ( 𝑥 ‘ 𝑎 ) ∈ ℂ )
11 5 6 10 fsumcom ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝑎 ) = Σ 𝑥 ∈ 𝐷 Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑥 ‘ 𝑎 ) )
12 eqid ⊢ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) )
13 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
14 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
15 1 2 3 12 4 13 14 sumdchr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝑎 ) = if ( 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( ♯ ‘ 𝐷 ) , 0 ) )
16 velsn ⊢ ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ↔ 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
17 ifbi ⊢ ( ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ↔ 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) = if ( 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( ♯ ‘ 𝐷 ) , 0 ) )
18 16 17 mp1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) = if ( 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( ♯ ‘ 𝐷 ) , 0 ) )
19 15 18 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝑎 ) = if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) )
20 19 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝑎 ) = Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) )
21 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
22 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
23 1 3 2 21 22 4 dchrsum ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷 ) → Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑥 ‘ 𝑎 ) = if ( 𝑥 = ( 0g ‘ 𝐺 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
24 velsn ⊢ ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ↔ 𝑥 = ( 0g ‘ 𝐺 ) )
25 ifbi ⊢ ( ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ↔ 𝑥 = ( 0g ‘ 𝐺 ) ) → if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝑥 = ( 0g ‘ 𝐺 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
26 24 25 mp1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝑥 = ( 0g ‘ 𝐺 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
27 23 26 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷 ) → Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑥 ‘ 𝑎 ) = if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) )
28 27 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑥 ∈ 𝐷 Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑥 ‘ 𝑎 ) = Σ 𝑥 ∈ 𝐷 if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) )
29 11 20 28 3eqtr3d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) = Σ 𝑥 ∈ 𝐷 if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) )
30 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
31 3 zncrng ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
32 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
33 4 12 ringidcl ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
34 30 31 32 33 4syl ⊢ ( 𝑁 ∈ ℕ → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
35 34 snssd ⊢ ( 𝑁 ∈ ℕ → { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ⊆ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
36 hashcl ⊢ ( 𝐷 ∈ Fin → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
37 nn0cn ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 → ( ♯ ‘ 𝐷 ) ∈ ℂ )
38 6 36 37 3syl ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐷 ) ∈ ℂ )
39 38 ralrimivw ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) ∈ ℂ )
40 5 olcd ⊢ ( 𝑁 ∈ ℕ → ( ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ) )
41 sumss2 ⊢ ( ( ( { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ⊆ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ∀ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) ∈ ℂ ) ∧ ( ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ) ) → Σ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) = Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) )
42 35 39 40 41 syl21anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) = Σ 𝑎 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) if ( 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } , ( ♯ ‘ 𝐷 ) , 0 ) )
43 1 dchrabl ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
44 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
45 2 21 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
46 43 44 45 3syl ⊢ ( 𝑁 ∈ ℕ → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
47 46 snssd ⊢ ( 𝑁 ∈ ℕ → { ( 0g ‘ 𝐺 ) } ⊆ 𝐷 )
48 phicl ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )
49 48 nncnd ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℂ )
50 49 ralrimivw ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) ∈ ℂ )
51 6 olcd ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝐷 ∈ Fin ) )
52 sumss2 ⊢ ( ( ( { ( 0g ‘ 𝐺 ) } ⊆ 𝐷 ∧ ∀ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) ∈ ℂ ) ∧ ( 𝐷 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝐷 ∈ Fin ) ) → Σ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) = Σ 𝑥 ∈ 𝐷 if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) )
53 47 50 51 52 syl21anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) = Σ 𝑥 ∈ 𝐷 if ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } , ( ϕ ‘ 𝑁 ) , 0 ) )
54 29 42 53 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) = Σ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) )
55 eqidd ⊢ ( 𝑎 = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) → ( ♯ ‘ 𝐷 ) = ( ♯ ‘ 𝐷 ) )
56 55 sumsn ⊢ ( ( ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℂ ) → Σ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) = ( ♯ ‘ 𝐷 ) )
57 34 38 56 syl2anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑎 ∈ { ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) } ( ♯ ‘ 𝐷 ) = ( ♯ ‘ 𝐷 ) )
58 eqidd ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ϕ ‘ 𝑁 ) = ( ϕ ‘ 𝑁 ) )
59 58 sumsn ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝐷 ∧ ( ϕ ‘ 𝑁 ) ∈ ℂ ) → Σ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) = ( ϕ ‘ 𝑁 ) )
60 46 49 59 syl2anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ( ϕ ‘ 𝑁 ) = ( ϕ ‘ 𝑁 ) )
61 54 57 60 3eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐷 ) = ( ϕ ‘ 𝑁 ) )