Proof of Theorem dchrptlem1
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑢 = 𝐶 → ((𝑃‘𝐼)‘𝑢) = ((𝑃‘𝐼)‘𝐶)) |
2 | 1 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑢 = 𝐶 → (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)))) |
3 | 2 | anbi1d 741 |
. . . . . 6
⊢ (𝑢 = 𝐶 → ((((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
4 | 3 | rexbidv 3052 |
. . . . 5
⊢ (𝑢 = 𝐶 → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
5 | 4 | iotabidv 5872 |
. . . 4
⊢ (𝑢 = 𝐶 → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
6 | | dchrpt.5 |
. . . 4
⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
7 | | iotaex 5868 |
. . . 4
⊢
(℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) ∈ V |
8 | 5, 6, 7 | fvmpt3i 6287 |
. . 3
⊢ (𝐶 ∈ 𝑈 → (𝑋‘𝐶) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
9 | 8 | ad2antlr 763 |
. 2
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
10 | | ovex 6678 |
. . 3
⊢ (𝑇↑𝑀) ∈ V |
11 | | simpr 477 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) |
12 | | simpllr 799 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) |
13 | 12 | simprd 479 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼))) |
14 | 11, 13 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼))) |
15 | | simp-4l 806 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝜑) |
16 | | simplr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝑚 ∈ ℤ) |
17 | 12 | simpld 475 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝑀 ∈ ℤ) |
18 | | dchrpt.n |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) |
19 | 18 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
20 | | dchrpt.z |
. . . . . . . . . . . . . . . . 17
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
21 | 20 | zncrng 19893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
22 | | crngring 18558 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
23 | | dchrpt.u |
. . . . . . . . . . . . . . . . 17
⊢ 𝑈 = (Unit‘𝑍) |
24 | | dchrpt.h |
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) |
25 | 23, 24 | unitgrp 18667 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) |
26 | 19, 21, 22, 25 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 ∈ Grp) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝐻 ∈ Grp) |
28 | | dchrpt.w |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈ Word 𝑈) |
29 | | wrdf 13310 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(#‘𝑊))⟶𝑈) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊:(0..^(#‘𝑊))⟶𝑈) |
31 | | dchrpt.i |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐼 ∈ dom 𝑊) |
32 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊:(0..^(#‘𝑊))⟶𝑈 → dom 𝑊 = (0..^(#‘𝑊))) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝑊 = (0..^(#‘𝑊))) |
34 | 31, 33 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 ∈ (0..^(#‘𝑊))) |
35 | 30, 34 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊‘𝐼) ∈ 𝑈) |
37 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑚 ∈ ℤ) |
38 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑀 ∈ ℤ) |
39 | 23, 24 | unitgrpbas 18666 |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Base‘𝐻) |
40 | | dchrpt.o |
. . . . . . . . . . . . . . 15
⊢ 𝑂 = (od‘𝐻) |
41 | | dchrpt.m |
. . . . . . . . . . . . . . 15
⊢ · =
(.g‘𝐻) |
42 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐻) = (0g‘𝐻) |
43 | 39, 40, 41, 42 | odcong 17968 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) ↔ (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)))) |
44 | 27, 36, 37, 38, 43 | syl112anc 1330 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) ↔ (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)))) |
45 | | dchrpt.t |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 =
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) |
46 | | neg1cn 11124 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℂ |
47 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
48 | | dchrpt.b |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐵 = (Base‘𝑍) |
49 | 20, 48 | znfi 19908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) |
50 | 18, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ Fin) |
51 | 48, 23 | unitss 18660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑈 ⊆ 𝐵 |
52 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) |
53 | 50, 51, 52 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑈 ∈ Fin) |
54 | 39, 40 | odcl2 17982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
55 | 26, 53, 35, 54 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ) |
57 | | nndivre 11056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
58 | 47, 56, 57 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ) |
59 | 58 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) |
60 | | cxpcl 24420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) →
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
61 | 46, 59, 60 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼)))) ∈ ℂ) |
62 | 45, 61 | syl5eqel 2705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑇 ∈ ℂ) |
63 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → -1 ∈
ℂ) |
64 | | neg1ne0 11126 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ≠
0 |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → -1 ≠ 0) |
66 | 63, 65, 59 | cxpne0d 24459 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼)))) ≠ 0) |
67 | 45 | neeq1i 2858 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ≠ 0 ↔
(-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0) |
68 | 66, 67 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑇 ≠ 0) |
69 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑚 − 𝑀) ∈ ℤ) |
70 | 69 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑚 − 𝑀) ∈ ℤ) |
71 | 38 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑀 ∈ ℤ) |
72 | | expaddz 12904 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ ((𝑚 − 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀))) |
73 | 62, 68, 70, 71, 72 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀))) |
74 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑚 ∈ ℤ) |
75 | 74 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑚 ∈ ℂ) |
76 | 71 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑀 ∈ ℂ) |
77 | 75, 76 | npcand 10396 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑚 − 𝑀) + 𝑀) = 𝑚) |
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = (𝑇↑𝑚)) |
79 | 45 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇↑(𝑚 − 𝑀)) = ((-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) |
80 | | root1eq1 24496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ (𝑚 − 𝑀) ∈ ℤ) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀))) |
81 | 55, 69, 80 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) →
(((-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀))) |
82 | 81 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((-1↑𝑐(2 /
(𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1) |
83 | 79, 82 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑(𝑚 − 𝑀)) = 1) |
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)) = (1 · (𝑇↑𝑀))) |
85 | 62, 68, 71 | expclzd 13013 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑𝑀) ∈ ℂ) |
86 | 85 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (1 · (𝑇↑𝑀)) = (𝑇↑𝑀)) |
87 | 84, 86 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)) = (𝑇↑𝑀)) |
88 | 73, 78, 87 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑𝑚) = (𝑇↑𝑀)) |
89 | 88 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) → (𝑇↑𝑚) = (𝑇↑𝑀))) |
90 | 44, 89 | sylbird 250 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)) → (𝑇↑𝑚) = (𝑇↑𝑀))) |
91 | 15, 16, 17, 90 | syl12anc 1324 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)) → (𝑇↑𝑚) = (𝑇↑𝑀))) |
92 | 14, 91 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑇↑𝑚) = (𝑇↑𝑀)) |
93 | 92 | eqeq2d 2632 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑚) ↔ ℎ = (𝑇↑𝑀))) |
94 | 93 | biimpd 219 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑚) → ℎ = (𝑇↑𝑀))) |
95 | 94 | expimpd 629 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) → ((((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) → ℎ = (𝑇↑𝑀))) |
96 | 95 | rexlimdva 3031 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) → ℎ = (𝑇↑𝑀))) |
97 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼))) |
98 | 97 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) |
99 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (𝑇↑𝑚) = (𝑇↑𝑀)) |
100 | 99 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (ℎ = (𝑇↑𝑚) ↔ ℎ = (𝑇↑𝑀))) |
101 | 98, 100 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ((((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ (((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑀)))) |
102 | 101 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ (((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑀))) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) |
103 | 102 | expr 643 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑀) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
104 | 103 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (ℎ = (𝑇↑𝑀) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) |
105 | 96, 104 | impbid 202 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ℎ = (𝑇↑𝑀))) |
106 | 105 | adantr 481 |
. . . 4
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ (𝑇↑𝑀) ∈ V) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ℎ = (𝑇↑𝑀))) |
107 | 106 | iota5 5871 |
. . 3
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ (𝑇↑𝑀) ∈ V) → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (𝑇↑𝑀)) |
108 | 10, 107 | mpan2 707 |
. 2
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (𝑇↑𝑀)) |
109 | 9, 108 | eqtrd 2656 |
1
⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀)) |