Proof of Theorem dchrabs
Step | Hyp | Ref
| Expression |
1 | | dchrabs.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
2 | | dchrabs.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | dchrabs.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
4 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑍) =
(Base‘𝑍) |
5 | | dchrabs.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
6 | 1, 2, 3, 4, 5 | dchrf 24967 |
. . . . . 6
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
7 | | dchrabs.u |
. . . . . . . 8
⊢ 𝑈 = (Unit‘𝑍) |
8 | 4, 7 | unitss 18660 |
. . . . . . 7
⊢ 𝑈 ⊆ (Base‘𝑍) |
9 | | dchrabs.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
10 | 8, 9 | sseldi 3601 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑍)) |
11 | 6, 10 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝑋‘𝐴) ∈ ℂ) |
12 | 1, 2, 3, 4, 7, 5, 10 | dchrn0 24975 |
. . . . . 6
⊢ (𝜑 → ((𝑋‘𝐴) ≠ 0 ↔ 𝐴 ∈ 𝑈)) |
13 | 9, 12 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝑋‘𝐴) ≠ 0) |
14 | 11, 13 | absrpcld 14187 |
. . . 4
⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ∈
ℝ+) |
15 | 1, 3 | dchrrcl 24965 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
16 | 2, 4 | znfi 19908 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(Base‘𝑍) ∈
Fin) |
17 | 5, 15, 16 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑍) ∈ Fin) |
18 | | ssfi 8180 |
. . . . . . 7
⊢
(((Base‘𝑍)
∈ Fin ∧ 𝑈 ⊆
(Base‘𝑍)) →
𝑈 ∈
Fin) |
19 | 17, 8, 18 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ Fin) |
20 | | hashcl 13147 |
. . . . . 6
⊢ (𝑈 ∈ Fin →
(#‘𝑈) ∈
ℕ0) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑈) ∈
ℕ0) |
22 | 21 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (#‘𝑈) ∈ ℝ) |
23 | 22 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (#‘𝑈) ∈ ℂ) |
24 | | ne0i 3921 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑈 → 𝑈 ≠ ∅) |
25 | 9, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ≠ ∅) |
26 | | hashnncl 13157 |
. . . . . . . 8
⊢ (𝑈 ∈ Fin →
((#‘𝑈) ∈ ℕ
↔ 𝑈 ≠
∅)) |
27 | 19, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝑈) ∈ ℕ ↔ 𝑈 ≠ ∅)) |
28 | 25, 27 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (#‘𝑈) ∈ ℕ) |
29 | 28 | nnne0d 11065 |
. . . . 5
⊢ (𝜑 → (#‘𝑈) ≠ 0) |
30 | 23, 29 | reccld 10794 |
. . . 4
⊢ (𝜑 → (1 / (#‘𝑈)) ∈
ℂ) |
31 | 14, 22, 30 | cxpmuld 24480 |
. . 3
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐((#‘𝑈) · (1 / (#‘𝑈)))) = (((abs‘(𝑋‘𝐴))↑𝑐(#‘𝑈))↑𝑐(1 /
(#‘𝑈)))) |
32 | 23, 29 | recidd 10796 |
. . . 4
⊢ (𝜑 → ((#‘𝑈) · (1 / (#‘𝑈))) = 1) |
33 | 32 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐((#‘𝑈) · (1 / (#‘𝑈)))) = ((abs‘(𝑋‘𝐴))↑𝑐1)) |
34 | 11 | abscld 14175 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ∈ ℝ) |
35 | 34 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ∈ ℂ) |
36 | | cxpexp 24414 |
. . . . . 6
⊢
(((abs‘(𝑋‘𝐴)) ∈ ℂ ∧ (#‘𝑈) ∈ ℕ0)
→ ((abs‘(𝑋‘𝐴))↑𝑐(#‘𝑈)) = ((abs‘(𝑋‘𝐴))↑(#‘𝑈))) |
37 | 35, 21, 36 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐(#‘𝑈)) = ((abs‘(𝑋‘𝐴))↑(#‘𝑈))) |
38 | 11, 21 | absexpd 14191 |
. . . . 5
⊢ (𝜑 → (abs‘((𝑋‘𝐴)↑(#‘𝑈))) = ((abs‘(𝑋‘𝐴))↑(#‘𝑈))) |
39 | | cnring 19768 |
. . . . . . . . . . 11
⊢
ℂfld ∈ Ring |
40 | | cnfldbas 19750 |
. . . . . . . . . . . . 13
⊢ ℂ =
(Base‘ℂfld) |
41 | | cnfld0 19770 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘ℂfld) |
42 | | cndrng 19775 |
. . . . . . . . . . . . 13
⊢
ℂfld ∈ DivRing |
43 | 40, 41, 42 | drngui 18753 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
44 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
45 | 43, 44 | unitsubm 18670 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) |
46 | 39, 45 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ ∖ {0})
∈ (SubMnd‘(mulGrp‘ℂfld))) |
47 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ ((𝑋‘𝐴) ∈ (ℂ ∖ {0}) ↔
((𝑋‘𝐴) ∈ ℂ ∧ (𝑋‘𝐴) ≠ 0)) |
48 | 11, 13, 47 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋‘𝐴) ∈ (ℂ ∖
{0})) |
49 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
50 | | eqid 2622 |
. . . . . . . . . . 11
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
51 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) =
(.g‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
52 | 49, 50, 51 | submmulg 17586 |
. . . . . . . . . 10
⊢
(((ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld)) ∧ (#‘𝑈) ∈ ℕ0
∧ (𝑋‘𝐴) ∈ (ℂ ∖ {0}))
→ ((#‘𝑈)(.g‘(mulGrp‘ℂfld))(𝑋‘𝐴)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))(𝑋‘𝐴))) |
53 | 46, 21, 48, 52 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑈)(.g‘(mulGrp‘ℂfld))(𝑋‘𝐴)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))(𝑋‘𝐴))) |
54 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
((mulGrp‘𝑍)
↾s 𝑈) =
((mulGrp‘𝑍)
↾s 𝑈) |
55 | 1, 2, 3, 7, 54, 50, 5 | dchrghm 24981 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (((mulGrp‘𝑍) ↾s 𝑈) GrpHom
((mulGrp‘ℂfld) ↾s (ℂ ∖
{0})))) |
56 | 21 | nn0zd 11480 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑈) ∈ ℤ) |
57 | 7, 54 | unitgrpbas 18666 |
. . . . . . . . . . . 12
⊢ 𝑈 =
(Base‘((mulGrp‘𝑍) ↾s 𝑈)) |
58 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(.g‘((mulGrp‘𝑍) ↾s 𝑈)) =
(.g‘((mulGrp‘𝑍) ↾s 𝑈)) |
59 | 57, 58, 51 | ghmmulg 17672 |
. . . . . . . . . . 11
⊢ (((𝑋 ↾ 𝑈) ∈ (((mulGrp‘𝑍) ↾s 𝑈) GrpHom
((mulGrp‘ℂfld) ↾s (ℂ ∖
{0}))) ∧ (#‘𝑈)
∈ ℤ ∧ 𝐴
∈ 𝑈) → ((𝑋 ↾ 𝑈)‘((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))((𝑋 ↾ 𝑈)‘𝐴))) |
60 | 55, 56, 9, 59 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ↾ 𝑈)‘((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))((𝑋 ↾ 𝑈)‘𝐴))) |
61 | 5, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) |
62 | 61 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
63 | 2 | zncrng 19893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
64 | | crngring 18558 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑍 ∈ Ring) |
66 | 7, 54 | unitgrp 18667 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ Ring →
((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((mulGrp‘𝑍) ↾s 𝑈) ∈ Grp) |
68 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(od‘((mulGrp‘𝑍) ↾s 𝑈)) = (od‘((mulGrp‘𝑍) ↾s 𝑈)) |
69 | 57, 68 | oddvds2 17983 |
. . . . . . . . . . . . . 14
⊢
((((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp ∧ 𝑈 ∈
Fin ∧ 𝐴 ∈ 𝑈) →
((od‘((mulGrp‘𝑍) ↾s 𝑈))‘𝐴) ∥ (#‘𝑈)) |
70 | 67, 19, 9, 69 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((od‘((mulGrp‘𝑍) ↾s 𝑈))‘𝐴) ∥ (#‘𝑈)) |
71 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(0g‘((mulGrp‘𝑍) ↾s 𝑈)) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈)) |
72 | 57, 68, 58, 71 | oddvds 17966 |
. . . . . . . . . . . . . 14
⊢
((((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp ∧ 𝐴 ∈
𝑈 ∧ (#‘𝑈) ∈ ℤ) →
(((od‘((mulGrp‘𝑍) ↾s 𝑈))‘𝐴) ∥ (#‘𝑈) ↔ ((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈)))) |
73 | 67, 9, 56, 72 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(((od‘((mulGrp‘𝑍) ↾s 𝑈))‘𝐴) ∥ (#‘𝑈) ↔ ((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈)))) |
74 | 70, 73 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈))) |
75 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑍) = (1r‘𝑍) |
76 | 7, 54, 75 | unitgrpid 18669 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ Ring →
(1r‘𝑍) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈))) |
77 | 65, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝑍) =
(0g‘((mulGrp‘𝑍) ↾s 𝑈))) |
78 | 74, 77 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴) = (1r‘𝑍)) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ↾ 𝑈)‘((#‘𝑈)(.g‘((mulGrp‘𝑍) ↾s 𝑈))𝐴)) = ((𝑋 ↾ 𝑈)‘(1r‘𝑍))) |
80 | | fvres 6207 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑈 → ((𝑋 ↾ 𝑈)‘𝐴) = (𝑋‘𝐴)) |
81 | 9, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ↾ 𝑈)‘𝐴) = (𝑋‘𝐴)) |
82 | 81 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))((𝑋 ↾ 𝑈)‘𝐴)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))(𝑋‘𝐴))) |
83 | 60, 79, 82 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ↾ 𝑈)‘(1r‘𝑍)) = ((#‘𝑈)(.g‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))(𝑋‘𝐴))) |
84 | 7, 75 | 1unit 18658 |
. . . . . . . . . 10
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ 𝑈) |
85 | | fvres 6207 |
. . . . . . . . . 10
⊢
((1r‘𝑍) ∈ 𝑈 → ((𝑋 ↾ 𝑈)‘(1r‘𝑍)) = (𝑋‘(1r‘𝑍))) |
86 | 65, 84, 85 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ↾ 𝑈)‘(1r‘𝑍)) = (𝑋‘(1r‘𝑍))) |
87 | 53, 83, 86 | 3eqtr2d 2662 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝑈)(.g‘(mulGrp‘ℂfld))(𝑋‘𝐴)) = (𝑋‘(1r‘𝑍))) |
88 | | cnfldexp 19779 |
. . . . . . . . 9
⊢ (((𝑋‘𝐴) ∈ ℂ ∧ (#‘𝑈) ∈ ℕ0)
→ ((#‘𝑈)(.g‘(mulGrp‘ℂfld))(𝑋‘𝐴)) = ((𝑋‘𝐴)↑(#‘𝑈))) |
89 | 11, 21, 88 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝑈)(.g‘(mulGrp‘ℂfld))(𝑋‘𝐴)) = ((𝑋‘𝐴)↑(#‘𝑈))) |
90 | 1, 2, 3 | dchrmhm 24966 |
. . . . . . . . . 10
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
91 | 90, 5 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
92 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
93 | 92, 75 | ringidval 18503 |
. . . . . . . . . 10
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
94 | | cnfld1 19771 |
. . . . . . . . . . 11
⊢ 1 =
(1r‘ℂfld) |
95 | 44, 94 | ringidval 18503 |
. . . . . . . . . 10
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
96 | 93, 95 | mhm0 17343 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑋‘(1r‘𝑍)) = 1) |
97 | 91, 96 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) |
98 | 87, 89, 97 | 3eqtr3d 2664 |
. . . . . . 7
⊢ (𝜑 → ((𝑋‘𝐴)↑(#‘𝑈)) = 1) |
99 | 98 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝑋‘𝐴)↑(#‘𝑈))) = (abs‘1)) |
100 | | abs1 14037 |
. . . . . 6
⊢
(abs‘1) = 1 |
101 | 99, 100 | syl6eq 2672 |
. . . . 5
⊢ (𝜑 → (abs‘((𝑋‘𝐴)↑(#‘𝑈))) = 1) |
102 | 37, 38, 101 | 3eqtr2d 2662 |
. . . 4
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐(#‘𝑈)) = 1) |
103 | 102 | oveq1d 6665 |
. . 3
⊢ (𝜑 → (((abs‘(𝑋‘𝐴))↑𝑐(#‘𝑈))↑𝑐(1 /
(#‘𝑈))) =
(1↑𝑐(1 / (#‘𝑈)))) |
104 | 31, 33, 103 | 3eqtr3d 2664 |
. 2
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐1) =
(1↑𝑐(1 / (#‘𝑈)))) |
105 | 35 | cxp1d 24452 |
. 2
⊢ (𝜑 → ((abs‘(𝑋‘𝐴))↑𝑐1) =
(abs‘(𝑋‘𝐴))) |
106 | 30 | 1cxpd 24453 |
. 2
⊢ (𝜑 →
(1↑𝑐(1 / (#‘𝑈))) = 1) |
107 | 104, 105,
106 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1) |