Step | Hyp | Ref
| Expression |
1 | | dchrpt.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
2 | | dchrpt.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | dchrpt.b |
. . 3
⊢ 𝐵 = (Base‘𝑍) |
4 | | dchrpt.u |
. . 3
⊢ 𝑈 = (Unit‘𝑍) |
5 | | dchrpt.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | dchrpt.d |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
7 | | fveq2 6717 |
. . 3
⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥)) |
8 | | fveq2 6717 |
. . 3
⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦)) |
9 | | fveq2 6717 |
. . 3
⊢ (𝑣 = (𝑥(.r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(.r‘𝑍)𝑦))) |
10 | | fveq2 6717 |
. . 3
⊢ (𝑣 = (1r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1r‘𝑍))) |
11 | | dchrpt.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻dom DProd 𝑆) |
12 | | zex 12185 |
. . . . . . . . . . . . 13
⊢ ℤ
∈ V |
13 | 12 | mptex 7039 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
14 | 13 | rnex 7690 |
. . . . . . . . . . 11
⊢ ran
(𝑛 ∈ ℤ ↦
(𝑛 · (𝑊‘𝑘))) ∈ V |
15 | | dchrpt.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) |
16 | 14, 15 | dmmpti 6522 |
. . . . . . . . . 10
⊢ dom 𝑆 = dom 𝑊 |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑆 = dom 𝑊) |
18 | | dchrpt.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐻dProj𝑆) |
19 | | dchrpt.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ dom 𝑊) |
20 | 11, 17, 18, 19 | dpjf 19444 |
. . . . . . . 8
⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼)) |
21 | | dchrpt.3 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) |
22 | 21 | feq2d 6531 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))) |
23 | 20, 22 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)) |
24 | 23 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼)) |
25 | 19 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊) |
26 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘))) |
27 | 26 | cbvmptv 5158 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) |
28 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼)) |
29 | 28 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼))) |
30 | 29 | mpteq2dv 5151 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
31 | 27, 30 | syl5eq 2790 |
. . . . . . . . 9
⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
32 | 31 | rneqd 5807 |
. . . . . . . 8
⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
33 | 32, 15, 14 | fvmpt3i 6823 |
. . . . . . 7
⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
34 | 25, 33 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
35 | 24, 34 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))) |
36 | | eqid 2737 |
. . . . . 6
⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) |
37 | | ovex 7246 |
. . . . . 6
⊢ (𝑎 · (𝑊‘𝐼)) ∈ V |
38 | 36, 37 | elrnmpti 5829 |
. . . . 5
⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
39 | 35, 38 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
40 | | dchrpt.1 |
. . . . . 6
⊢ 1 =
(1r‘𝑍) |
41 | | dchrpt.n1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 1 ) |
42 | | dchrpt.h |
. . . . . 6
⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) |
43 | | dchrpt.m |
. . . . . 6
⊢ · =
(.g‘𝐻) |
44 | | dchrpt.au |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
45 | | dchrpt.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝑈) |
46 | | dchrpt.o |
. . . . . 6
⊢ 𝑂 = (od‘𝐻) |
47 | | dchrpt.t |
. . . . . 6
⊢ 𝑇 =
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) |
48 | | dchrpt.4 |
. . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) |
49 | | dchrpt.5 |
. . . . . 6
⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
50 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎)) |
51 | | neg1cn 11944 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
52 | | 2re 11904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
53 | 5 | nnnn0d 12150 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
54 | 2 | zncrng 20509 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
55 | | crngring 19574 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ Ring) |
57 | 4, 42 | unitgrp 19685 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Grp) |
59 | 2, 3 | znfi 20524 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) |
60 | 5, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ Fin) |
61 | 3, 4 | unitss 19678 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ 𝐵 |
62 | | ssfi 8851 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) |
63 | 60, 61, 62 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ Fin) |
64 | | wrdf 14074 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈) |
65 | 45, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈) |
66 | 65 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
67 | 19, 66 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊))) |
68 | 65, 67 | ffvelrnd 6905 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈) |
69 | 4, 42 | unitgrpbas 19684 |
. . . . . . . . . . . . 13
⊢ 𝑈 = (Base‘𝐻) |
70 | 69, 46 | odcl2 18956 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
71 | 58, 63, 68, 70 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
72 | | nndivre 11871 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
73 | 52, 71, 72 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
74 | 73 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) |
75 | | cxpcl 25562 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
76 | 51, 74, 75 | sylancr 590 |
. . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
77 | 47, 76 | eqeltrid 2842 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℂ) |
78 | 77 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ) |
79 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) |
80 | | neg1ne0 11946 |
. . . . . . . . . 10
⊢ -1 ≠
0 |
81 | 80 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ≠
0) |
82 | 79, 81, 74 | cxpne0d 25601 |
. . . . . . . 8
⊢ (𝜑 →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) |
83 | 47 | neeq1i 3005 |
. . . . . . . 8
⊢ (𝑇 ≠ 0 ↔
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) |
84 | 82, 83 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ≠ 0) |
85 | 84 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0) |
86 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) |
87 | 78, 85, 86 | expclzd 13721 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ) |
88 | 50, 87 | eqeltrd 2838 |
. . . 4
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ) |
89 | 39, 88 | rexlimddv 3210 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ) |
90 | | fveqeq2 6726 |
. . . . . 6
⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) |
91 | 90 | rexbidv 3216 |
. . . . 5
⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) |
92 | 39 | ralrimiva 3105 |
. . . . . 6
⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
93 | 92 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼))) |
94 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
95 | 91, 93, 94 | rspcdva 3539 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) |
96 | | fveqeq2 6726 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) |
97 | 96 | rexbidv 3216 |
. . . . . 6
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)))) |
98 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼))) |
99 | 98 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
100 | 99 | cbvrexvw 3359 |
. . . . . 6
⊢
(∃𝑎 ∈
ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
101 | 97, 100 | bitrdi 290 |
. . . . 5
⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
102 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
103 | 101, 93, 102 | rspcdva 3539 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
104 | | reeanv 3279 |
. . . . 5
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) |
105 | 77 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ) |
106 | 84 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0) |
107 | | simprll 779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ) |
108 | | simprlr 780 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ) |
109 | | expaddz 13679 |
. . . . . . . . 9
⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
110 | 105, 106,
107, 108, 109 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
111 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑) |
112 | 56 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring) |
113 | 94 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈) |
114 | 102 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈) |
115 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑍) = (.r‘𝑍) |
116 | 4, 115 | unitmulcl 19682 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) |
117 | 112, 113,
114, 116 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) |
118 | 107, 108 | zaddcld 12286 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ) |
119 | | simprrl 781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))) |
120 | | simprrr 782 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) |
121 | 119, 120 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
122 | 11, 17, 18, 19 | dpjghm 19450 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻)) |
123 | 21 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = (𝐻 ↾s 𝑈)) |
124 | 42 | ovexi 7247 |
. . . . . . . . . . . . . . . 16
⊢ 𝐻 ∈ V |
125 | 69 | ressid 16796 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ V → (𝐻 ↾s 𝑈) = 𝐻) |
126 | 124, 125 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 ↾s 𝑈) = 𝐻 |
127 | 123, 126 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻 ↾s (𝐻 DProd 𝑆)) = 𝐻) |
128 | 127 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐻 ↾s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻)) |
129 | 122, 128 | eleqtrd 2840 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) |
130 | 129 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻)) |
131 | 4 | fvexi 6731 |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ V |
132 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
133 | 132, 115 | mgpplusg 19508 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
134 | 42, 133 | ressplusg 16834 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ V →
(.r‘𝑍) =
(+g‘𝐻)) |
135 | 131, 134 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(.r‘𝑍) = (+g‘𝐻) |
136 | 69, 135, 135 | ghmlin 18627 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) |
137 | 130, 113,
114, 136 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(.r‘𝑍)((𝑃‘𝐼)‘𝑦))) |
138 | 58 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp) |
139 | 68 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈) |
140 | 69, 43, 135 | mulgdir 18523 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
141 | 138, 107,
108, 139, 140 | syl13anc 1374 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(.r‘𝑍)(𝑏 · (𝑊‘𝐼)))) |
142 | 121, 137,
141 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼))) |
143 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥(.r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) |
144 | 111, 117,
118, 142, 143 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏))) |
145 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎)) |
146 | 111, 113,
107, 119, 145 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎)) |
147 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏)) |
148 | 111, 114,
108, 120, 147 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏)) |
149 | 146, 148 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏))) |
150 | 110, 144,
149 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
151 | 150 | expr 460 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
152 | 151 | rexlimdvva 3213 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
153 | 104, 152 | syl5bir 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
154 | 95, 103, 153 | mp2and 699 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
155 | | id 22 |
. . . . 5
⊢ (𝜑 → 𝜑) |
156 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑍) = (1r‘𝑍) |
157 | 4, 156 | 1unit 19676 |
. . . . . 6
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ 𝑈) |
158 | 56, 157 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑍) ∈ 𝑈) |
159 | | 0zd 12188 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
160 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐻) = (0g‘𝐻) |
161 | 160, 160 | ghmid 18628 |
. . . . . . 7
⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) |
162 | 129, 161 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(0g‘𝐻)) = (0g‘𝐻)) |
163 | 4, 42, 156 | unitgrpid 19687 |
. . . . . . . 8
⊢ (𝑍 ∈ Ring →
(1r‘𝑍) =
(0g‘𝐻)) |
164 | 56, 163 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑍) = (0g‘𝐻)) |
165 | 164 | fveq2d 6721 |
. . . . . 6
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = ((𝑃‘𝐼)‘(0g‘𝐻))) |
166 | 69, 160, 43 | mulg0 18495 |
. . . . . . 7
⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) |
167 | 68, 166 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0g‘𝐻)) |
168 | 162, 165,
167 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼))) |
169 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . 5
⊢ (((𝜑 ∧ (1r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) |
170 | 155, 158,
159, 168, 169 | syl22anc 839 |
. . . 4
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = (𝑇↑0)) |
171 | 77 | exp0d 13710 |
. . . 4
⊢ (𝜑 → (𝑇↑0) = 1) |
172 | 170, 171 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) |
173 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
89, 154, 172 | dchrelbasd 26120 |
. 2
⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷) |
174 | 61, 44 | sseldi 3899 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
175 | | eleq1 2825 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈)) |
176 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴)) |
177 | 175, 176 | ifbieq1d 4463 |
. . . . . 6
⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
178 | | eqid 2737 |
. . . . . 6
⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) |
179 | | fvex 6730 |
. . . . . . 7
⊢ (𝑋‘𝑣) ∈ V |
180 | | c0ex 10827 |
. . . . . . 7
⊢ 0 ∈
V |
181 | 179, 180 | ifex 4489 |
. . . . . 6
⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V |
182 | 177, 178,
181 | fvmpt3i 6823 |
. . . . 5
⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
183 | 174, 182 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0)) |
184 | 44 | iftrued 4447 |
. . . 4
⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴)) |
185 | 183, 184 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴)) |
186 | | fveqeq2 6726 |
. . . . . 6
⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) |
187 | 186 | rexbidv 3216 |
. . . . 5
⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) |
188 | 187, 92, 44 | rspcdva 3539 |
. . . 4
⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) |
189 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26145 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎)) |
190 | 47 | oveq1i 7223 |
. . . . . . . 8
⊢ (𝑇↑𝑎) = ((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) |
191 | 189, 190 | eqtrdi 2794 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼))))↑𝑎)) |
192 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) |
193 | 58 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp) |
194 | 68 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈) |
195 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ) |
196 | 69, 46, 43, 160 | oddvds 18939 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
197 | 193, 194,
195, 196 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
198 | 71 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
199 | | root1eq1 25641 |
. . . . . . . . . . 11
⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) |
200 | 198, 195,
199 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎)) |
201 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))) |
202 | 40, 164 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 =
(0g‘𝐻)) |
203 | 202 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 =
(0g‘𝐻)) |
204 | 201, 203 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0g‘𝐻))) |
205 | 197, 200,
204 | 3bitr4d 314 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 )) |
206 | 205 | necon3bid 2985 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 )) |
207 | 192, 206 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑𝑐(2
/ (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1) |
208 | 191, 207 | eqnetrd 3008 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1) |
209 | 208 | rexlimdvaa 3204 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) |
210 | 44, 209 | mpdan 687 |
. . . 4
⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1)) |
211 | 188, 210 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑋‘𝐴) ≠ 1) |
212 | 185, 211 | eqnetrd 3008 |
. 2
⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) |
213 | | fveq1 6716 |
. . . 4
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴)) |
214 | 213 | neeq1d 3000 |
. . 3
⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)) |
215 | 214 | rspcev 3537 |
. 2
⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
216 | 173, 212,
215 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |