Metamath Proof Explorer

Theorem dchrabs

Description: A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrabs.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrabs.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrabs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrabs.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrabs.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrabs.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion dchrabs ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 dchrabs.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrabs.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 dchrabs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
4 dchrabs.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
5 dchrabs.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
6 dchrabs.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
8 1 4 2 7 3 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
9 7 5 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
10 9 6 sseldi ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑍 ) )
11 8 10 ffvelrnd ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ∈ ℂ )
12 1 4 2 7 5 3 10 dchrn0 ⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ 𝑈 ) )
13 6 12 mpbird ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ≠ 0 )
14 11 13 absrpcld ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℝ+ )
15 1 2 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
16 4 7 znfi ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ 𝑍 ) ∈ Fin )
17 3 15 16 3syl ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) ∈ Fin )
18 ssfi ⊢ ( ( ( Base ‘ 𝑍 ) ∈ Fin ∧ 𝑈 ⊆ ( Base ‘ 𝑍 ) ) → 𝑈 ∈ Fin )
19 17 9 18 sylancl ⊢ ( 𝜑 → 𝑈 ∈ Fin )
20 hashcl ⊢ ( 𝑈 ∈ Fin → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
21 19 20 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
22 21 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℂ )
24 6 ne0d ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
25 hashnncl ⊢ ( 𝑈 ∈ Fin → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
26 19 25 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
27 24 26 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ )
28 27 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ≠ 0 )
29 23 28 reccld ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝑈 ) ) ∈ ℂ )
30 14 22 29 cxpmuld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) ) = ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
31 23 28 recidd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) = 1 )
32 31 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) )
33 11 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℝ )
34 33 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℂ )
35 cxpexp ⊢ ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
36 34 21 35 syl2anc ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
37 11 21 absexpd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
38 cnring ⊢ ℂfld ∈ Ring
39 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
40 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
41 cndrng ⊢ ℂfld ∈ DivRing
42 39 40 41 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
43 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
44 42 43 unitsubm ⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
45 38 44 mp1i ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
46 eldifsn ⊢ ( ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) )
47 11 13 46 sylanbrc ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) )
48 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
49 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
50 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) = ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
51 48 49 50 submmulg ⊢ ( ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ∧ ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
52 45 21 47 51 syl3anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
53 eqid ⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
54 1 4 2 5 53 49 3 dchrghm ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) )
55 21 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℤ )
56 5 53 unitgrpbas ⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
57 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
58 56 57 50 ghmmulg ⊢ ( ( ( 𝑋 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℤ ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) )
59 54 55 6 58 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) )
60 3 15 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
61 60 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
62 4 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
63 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
64 61 62 63 3syl ⊢ ( 𝜑 → 𝑍 ∈ Ring )
65 5 53 unitgrp ⊢ ( 𝑍 ∈ Ring → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
66 64 65 syl ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
67 eqid ⊢ ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
68 56 67 oddvds2 ⊢ ( ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑈 ∈ Fin ∧ 𝐴 ∈ 𝑈 ) → ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) )
69 66 19 6 68 syl3anc ⊢ ( 𝜑 → ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) )
70 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
71 56 67 57 70 oddvds ⊢ ( ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp ∧ 𝐴 ∈ 𝑈 ∧ ( ♯ ‘ 𝑈 ) ∈ ℤ ) → ( ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) ↔ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ) )
72 66 6 55 71 syl3anc ⊢ ( 𝜑 → ( ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) ↔ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ) )
73 69 72 mpbid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
74 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
75 5 53 74 unitgrpid ⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
76 64 75 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
77 73 76 eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 1r ‘ 𝑍 ) )
78 77 fveq2d ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) )
79 6 fvresd ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
80 79 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
81 59 78 80 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
82 5 74 1unit ⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
83 fvres ⊢ ( ( 1r ‘ 𝑍 ) ∈ 𝑈 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
84 64 82 83 3syl ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
85 52 81 84 3eqtr2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
86 cnfldexp ⊢ ( ( ( 𝑋 ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) )
87 11 21 86 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) )
88 1 4 2 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
89 88 3 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
90 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
91 90 74 ringidval ⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
92 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
93 43 92 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
94 91 93 mhm0 ⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
95 89 94 syl ⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
96 85 87 95 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) = 1 )
97 96 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = ( abs ‘ 1 ) )
98 abs1 ⊢ ( abs ‘ 1 ) = 1
99 97 98 eqtrdi ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = 1 )
100 36 37 99 3eqtr2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = 1 )
101 100 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) = ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
102 30 32 101 3eqtr3d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) = ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
103 34 cxp1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) = ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) )
104 29 1cxpd ⊢ ( 𝜑 → ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) = 1 )
105 102 103 104 3eqtr3d ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 1 )