Step | Hyp | Ref
| Expression |
1 | | cycpmco2.c |
. . . 4
⊢ 𝑀 = (toCyc‘𝐷) |
2 | | cycpmco2.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
3 | | cycpmco2.1 |
. . . . 5
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
4 | | ssrab2 3969 |
. . . . . . 7
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
5 | | cycpmco2.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
6 | | cycpmco2.s |
. . . . . . . . . . 11
⊢ 𝑆 = (SymGrp‘𝐷) |
7 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
8 | 1, 6, 7 | tocycf 30963 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
9 | 2, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
10 | 9 | fdmd 6515 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
11 | 5, 10 | eleqtrd 2835 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
12 | 4, 11 | sseldi 3875 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
13 | | cycpmco2.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
14 | 13 | eldifad 3855 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
15 | 14 | s1cld 14048 |
. . . . . 6
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
16 | | splcl 14205 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
17 | 12, 15, 16 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
18 | 3, 17 | eqeltrid 2837 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Word 𝐷) |
19 | | cycpmco2.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
20 | | cycpmco2.e |
. . . . 5
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
21 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2f1 30970 |
. . . 4
⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) |
22 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
23 | | dmeq 5746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
24 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
25 | 22, 23, 24 | f1eq123d 6612 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
26 | 25 | elrab 3588 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
27 | 11, 26 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
28 | 27 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
29 | | f1cnv 6643 |
. . . . . . . . . . . 12
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
30 | | f1of 6620 |
. . . . . . . . . . . 12
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
32 | 31, 19 | ffvelrnd 6864 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
33 | | wrddm 13964 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
34 | 12, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
35 | 32, 34 | eleqtrd 2835 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
36 | | fzofzp1 13227 |
. . . . . . . . 9
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
38 | 20, 37 | eqeltrid 2837 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
39 | | elfzuz3 12997 |
. . . . . . 7
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐸)) |
40 | | fzoss2 13158 |
. . . . . . 7
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝐸) → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) |
42 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2lem3 30974 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) |
43 | 42 | oveq2d 7188 |
. . . . . 6
⊢ (𝜑 → (0..^((♯‘𝑈) − 1)) =
(0..^(♯‘𝑊))) |
44 | 41, 43 | sseqtrrd 3918 |
. . . . 5
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^((♯‘𝑈) − 1))) |
45 | | cycpmco2lem7.3 |
. . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^𝐸)) |
46 | 44, 45 | sseldd 3878 |
. . . 4
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^((♯‘𝑈) − 1))) |
47 | 1, 2, 18, 21, 46 | cycpmfv1 30959 |
. . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = (𝑈‘((◡𝑈‘𝐾) + 1))) |
48 | | cycpmco2lem7.1 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ran 𝑊) |
49 | | f1f1orn 6631 |
. . . . . . 7
⊢ (𝑈:dom 𝑈–1-1→𝐷 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) |
50 | 21, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) |
51 | | ssun1 4062 |
. . . . . . . 8
⊢ ran 𝑊 ⊆ (ran 𝑊 ∪ {𝐼}) |
52 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2rn 30971 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) |
53 | 51, 52 | sseqtrrid 3930 |
. . . . . . 7
⊢ (𝜑 → ran 𝑊 ⊆ ran 𝑈) |
54 | 53 | sselda 3877 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → 𝐾 ∈ ran 𝑈) |
55 | | f1ocnvfv2 7047 |
. . . . . 6
⊢ ((𝑈:dom 𝑈–1-1-onto→ran
𝑈 ∧ 𝐾 ∈ ran 𝑈) → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) |
56 | 50, 54, 55 | syl2an2r 685 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) |
57 | 56 | fveq2d 6680 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = ((𝑀‘𝑈)‘𝐾)) |
58 | 48, 57 | mpdan 687 |
. . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = ((𝑀‘𝑈)‘𝐾)) |
59 | | f1f1orn 6631 |
. . . . . . . 8
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
60 | 28, 59 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
61 | 41, 34 | sseqtrrd 3918 |
. . . . . . . 8
⊢ (𝜑 → (0..^𝐸) ⊆ dom 𝑊) |
62 | 61, 45 | sseldd 3878 |
. . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ dom 𝑊) |
63 | | f1ocnvfv1 7046 |
. . . . . . 7
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ (◡𝑈‘𝐾) ∈ dom 𝑊) → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑈‘𝐾)) |
64 | 60, 62, 63 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑈‘𝐾)) |
65 | 3 | fveq1i 6677 |
. . . . . . . . 9
⊢ (𝑈‘(◡𝑈‘𝐾)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(◡𝑈‘𝐾)) |
66 | | fz0ssnn0 13095 |
. . . . . . . . . . . 12
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
67 | 66, 38 | sseldi 3875 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
68 | | nn0fz0 13098 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ ℕ0
↔ 𝐸 ∈ (0...𝐸)) |
69 | 67, 68 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ (0...𝐸)) |
70 | 12, 69, 38, 15, 45 | splfv1 14208 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(◡𝑈‘𝐾)) = (𝑊‘(◡𝑈‘𝐾))) |
71 | 65, 70 | syl5eq 2785 |
. . . . . . . 8
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = (𝑊‘(◡𝑈‘𝐾))) |
72 | 48, 56 | mpdan 687 |
. . . . . . . 8
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) |
73 | 71, 72 | eqtr3d 2775 |
. . . . . . 7
⊢ (𝜑 → (𝑊‘(◡𝑈‘𝐾)) = 𝐾) |
74 | 73 | fveq2d 6680 |
. . . . . 6
⊢ (𝜑 → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑊‘𝐾)) |
75 | 64, 74 | eqtr3d 2775 |
. . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) = (◡𝑊‘𝐾)) |
76 | 75 | oveq1d 7187 |
. . . 4
⊢ (𝜑 → ((◡𝑈‘𝐾) + 1) = ((◡𝑊‘𝐾) + 1)) |
77 | 76 | fveq2d 6680 |
. . 3
⊢ (𝜑 → (𝑈‘((◡𝑈‘𝐾) + 1)) = (𝑈‘((◡𝑊‘𝐾) + 1))) |
78 | 47, 58, 77 | 3eqtr3d 2781 |
. 2
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = (𝑈‘((◡𝑊‘𝐾) + 1))) |
79 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)) |
80 | 79 | fveq1d 6678 |
. . . 4
⊢ (𝜑 → (𝑈‘((◡𝑊‘𝐾) + 1)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((◡𝑊‘𝐾) + 1))) |
81 | 38 | elfzelzd 13001 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℤ) |
82 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) |
83 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 = ((◡𝑊‘𝐽) + 1)) |
84 | 83 | oveq1d 7187 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 − 1) = (((◡𝑊‘𝐽) + 1) − 1)) |
85 | | elfzonn0 13175 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → (◡𝑊‘𝐽) ∈
ℕ0) |
86 | 35, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑊‘𝐽) ∈
ℕ0) |
87 | 86 | nn0cnd 12040 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ ℂ) |
88 | | 1cnd 10716 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
89 | 87, 88 | pncand 11078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((◡𝑊‘𝐽) + 1) − 1) = (◡𝑊‘𝐽)) |
90 | 84, 89 | eqtr2d 2774 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑊‘𝐽) = (𝐸 − 1)) |
91 | 90 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑊‘𝐽) = (𝐸 − 1)) |
92 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) = (𝐸 − 1)) |
93 | 75 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) = (◡𝑊‘𝐾)) |
94 | 91, 92, 93 | 3eqtr2rd 2780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑊‘𝐾) = (◡𝑊‘𝐽)) |
95 | 94 | fveq2d 6680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐾)) = (𝑊‘(◡𝑊‘𝐽))) |
96 | | f1ocnvfv2 7047 |
. . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐾 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) |
97 | 60, 48, 96 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) |
98 | 97 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) |
99 | | f1ocnvfv2 7047 |
. . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐽 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
100 | 60, 19, 99 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
101 | 100 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
102 | 95, 98, 101 | 3eqtr3d 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → 𝐾 = 𝐽) |
103 | | cycpmco2lem7.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≠ 𝐽) |
104 | 103 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → 𝐾 ≠ 𝐽) |
105 | 102, 104 | pm2.21ddne 3018 |
. . . . . . . 8
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) |
106 | | 0zd 12076 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
107 | | nn0p1nn 12017 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) |
108 | 86, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) |
109 | 20, 108 | eqeltrid 2837 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℕ) |
110 | | 0p1e1 11840 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
111 | 110 | fveq2i 6679 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
112 | | nnuz 12365 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
113 | 111, 112 | eqtr4i 2764 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(0 + 1)) = ℕ |
114 | 109, 113 | eleqtrrdi 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ (ℤ≥‘(0 +
1))) |
115 | | fzosplitsnm1 13205 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝐸
∈ (ℤ≥‘(0 + 1))) → (0..^𝐸) = ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) |
116 | 106, 114,
115 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^𝐸) = ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) |
117 | 45, 116 | eleqtrd 2835 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) |
118 | | fvex 6689 |
. . . . . . . . . 10
⊢ (◡𝑈‘𝐾) ∈ V |
119 | | elunsn 30434 |
. . . . . . . . . 10
⊢ ((◡𝑈‘𝐾) ∈ V → ((◡𝑈‘𝐾) ∈ ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)}) ↔ ((◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1)) ∨ (◡𝑈‘𝐾) = (𝐸 − 1)))) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . 9
⊢ ((◡𝑈‘𝐾) ∈ ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)}) ↔ ((◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1)) ∨ (◡𝑈‘𝐾) = (𝐸 − 1))) |
121 | 117, 120 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1)) ∨ (◡𝑈‘𝐾) = (𝐸 − 1))) |
122 | 82, 105, 121 | mpjaodan 958 |
. . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) |
123 | | elfzom1elp1fzo 13197 |
. . . . . . 7
⊢ ((𝐸 ∈ ℤ ∧ (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) → ((◡𝑈‘𝐾) + 1) ∈ (0..^𝐸)) |
124 | 81, 122, 123 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((◡𝑈‘𝐾) + 1) ∈ (0..^𝐸)) |
125 | 76, 124 | eqeltrrd 2834 |
. . . . 5
⊢ (𝜑 → ((◡𝑊‘𝐾) + 1) ∈ (0..^𝐸)) |
126 | 12, 69, 38, 15, 125 | splfv1 14208 |
. . . 4
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((◡𝑊‘𝐾) + 1)) = (𝑊‘((◡𝑊‘𝐾) + 1))) |
127 | 80, 126 | eqtrd 2773 |
. . 3
⊢ (𝜑 → (𝑈‘((◡𝑊‘𝐾) + 1)) = (𝑊‘((◡𝑊‘𝐾) + 1))) |
128 | | 1zzd 12096 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
129 | 81, 128 | zsubcld 12175 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 − 1) ∈ ℤ) |
130 | | lencl 13976 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
131 | | nn0fz0 13098 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
132 | 131 | biimpi 219 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
133 | 12, 130, 132 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
134 | 133 | elfzelzd 13001 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) |
135 | 134, 128 | zsubcld 12175 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝑊) − 1) ∈
ℤ) |
136 | 109 | nnred 11733 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℝ) |
137 | 134 | zred 12170 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) |
138 | | 1red 10722 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
139 | | elfzle2 13004 |
. . . . . . . . . 10
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ 𝐸 ≤
(♯‘𝑊)) |
140 | 38, 139 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ≤ (♯‘𝑊)) |
141 | 136, 137,
138, 140 | lesub1dd 11336 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 − 1) ≤ ((♯‘𝑊) − 1)) |
142 | | eluz 12340 |
. . . . . . . . 9
⊢ (((𝐸 − 1) ∈ ℤ ∧
((♯‘𝑊) −
1) ∈ ℤ) → (((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1)) ↔ (𝐸 − 1) ≤ ((♯‘𝑊) − 1))) |
143 | 142 | biimpar 481 |
. . . . . . . 8
⊢ ((((𝐸 − 1) ∈ ℤ ∧
((♯‘𝑊) −
1) ∈ ℤ) ∧ (𝐸
− 1) ≤ ((♯‘𝑊) − 1)) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1))) |
144 | 129, 135,
141, 143 | syl21anc 837 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1))) |
145 | | fzoss2 13158 |
. . . . . . 7
⊢
(((♯‘𝑊)
− 1) ∈ (ℤ≥‘(𝐸 − 1)) → (0..^(𝐸 − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) |
146 | 144, 145 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0..^(𝐸 − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) |
147 | 146, 122 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^((♯‘𝑊) − 1))) |
148 | 75, 147 | eqeltrrd 2834 |
. . . 4
⊢ (𝜑 → (◡𝑊‘𝐾) ∈ (0..^((♯‘𝑊) − 1))) |
149 | 1, 2, 12, 28, 148 | cycpmfv1 30959 |
. . 3
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐾))) = (𝑊‘((◡𝑊‘𝐾) + 1))) |
150 | 97 | fveq2d 6680 |
. . 3
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐾))) = ((𝑀‘𝑊)‘𝐾)) |
151 | 127, 149,
150 | 3eqtr2rd 2780 |
. 2
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐾) = (𝑈‘((◡𝑊‘𝐾) + 1))) |
152 | 78, 151 | eqtr4d 2776 |
1
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾)) |