| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cycpmco2.c | . . . 4
⊢ 𝑀 = (toCyc‘𝐷) | 
| 2 |  | cycpmco2.d | . . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 3 |  | cycpmco2.1 | . . . . 5
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) | 
| 4 |  | ssrab2 4079 | . . . . . . 7
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 | 
| 5 |  | cycpmco2.w | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) | 
| 6 |  | cycpmco2.s | . . . . . . . . . . 11
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 7 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 8 | 1, 6, 7 | tocycf 33138 | . . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) | 
| 9 | 2, 8 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) | 
| 10 | 9 | fdmd 6745 | . . . . . . . 8
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 11 | 5, 10 | eleqtrd 2842 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 12 | 4, 11 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) | 
| 13 |  | cycpmco2.i | . . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) | 
| 14 | 13 | eldifad 3962 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝐷) | 
| 15 | 14 | s1cld 14642 | . . . . . 6
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) | 
| 16 |  | splcl 14791 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) | 
| 17 | 12, 15, 16 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) | 
| 18 | 3, 17 | eqeltrid 2844 | . . . 4
⊢ (𝜑 → 𝑈 ∈ Word 𝐷) | 
| 19 |  | cycpmco2.j | . . . . 5
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) | 
| 20 |  | cycpmco2.e | . . . . 5
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) | 
| 21 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2f1 33145 | . . . 4
⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) | 
| 22 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | 
| 23 |  | dmeq 5913 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) | 
| 24 |  | eqidd 2737 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) | 
| 25 | 22, 23, 24 | f1eq123d 6839 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 26 | 25 | elrab 3691 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 27 | 11, 26 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 28 | 27 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) | 
| 29 |  | f1cnv 6871 | . . . . . . . . . . . 12
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) | 
| 30 |  | f1of 6847 | . . . . . . . . . . . 12
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 31 | 28, 29, 30 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 32 | 31, 19 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) | 
| 33 |  | wrddm 14560 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 34 | 12, 33 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 35 | 32, 34 | eleqtrd 2842 | . . . . . . . . 9
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) | 
| 36 |  | fzofzp1 13804 | . . . . . . . . 9
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 37 | 35, 36 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 38 | 20, 37 | eqeltrid 2844 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) | 
| 39 |  | elfzuz3 13562 | . . . . . . 7
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐸)) | 
| 40 |  | fzoss2 13728 | . . . . . . 7
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝐸) → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) | 
| 41 | 38, 39, 40 | 3syl 18 | . . . . . 6
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^(♯‘𝑊))) | 
| 42 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2lem3 33149 | . . . . . . 7
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) | 
| 43 | 42 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (0..^((♯‘𝑈) − 1)) =
(0..^(♯‘𝑊))) | 
| 44 | 41, 43 | sseqtrrd 4020 | . . . . 5
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^((♯‘𝑈) − 1))) | 
| 45 |  | cycpmco2lem7.3 | . . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^𝐸)) | 
| 46 | 44, 45 | sseldd 3983 | . . . 4
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^((♯‘𝑈) − 1))) | 
| 47 | 1, 2, 18, 21, 46 | cycpmfv1 33134 | . . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = (𝑈‘((◡𝑈‘𝐾) + 1))) | 
| 48 |  | cycpmco2lem7.1 | . . . 4
⊢ (𝜑 → 𝐾 ∈ ran 𝑊) | 
| 49 |  | f1f1orn 6858 | . . . . . . 7
⊢ (𝑈:dom 𝑈–1-1→𝐷 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) | 
| 50 | 21, 49 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) | 
| 51 |  | ssun1 4177 | . . . . . . . 8
⊢ ran 𝑊 ⊆ (ran 𝑊 ∪ {𝐼}) | 
| 52 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2rn 33146 | . . . . . . . 8
⊢ (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) | 
| 53 | 51, 52 | sseqtrrid 4026 | . . . . . . 7
⊢ (𝜑 → ran 𝑊 ⊆ ran 𝑈) | 
| 54 | 53 | sselda 3982 | . . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → 𝐾 ∈ ran 𝑈) | 
| 55 |  | f1ocnvfv2 7298 | . . . . . 6
⊢ ((𝑈:dom 𝑈–1-1-onto→ran
𝑈 ∧ 𝐾 ∈ ran 𝑈) → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) | 
| 56 | 50, 54, 55 | syl2an2r 685 | . . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) | 
| 57 | 56 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = ((𝑀‘𝑈)‘𝐾)) | 
| 58 | 48, 57 | mpdan 687 | . . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = ((𝑀‘𝑈)‘𝐾)) | 
| 59 |  | f1f1orn 6858 | . . . . . . . 8
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) | 
| 60 | 28, 59 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) | 
| 61 | 41, 34 | sseqtrrd 4020 | . . . . . . . 8
⊢ (𝜑 → (0..^𝐸) ⊆ dom 𝑊) | 
| 62 | 61, 45 | sseldd 3983 | . . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ dom 𝑊) | 
| 63 |  | f1ocnvfv1 7297 | . . . . . . 7
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ (◡𝑈‘𝐾) ∈ dom 𝑊) → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑈‘𝐾)) | 
| 64 | 60, 62, 63 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑈‘𝐾)) | 
| 65 | 3 | fveq1i 6906 | . . . . . . . . 9
⊢ (𝑈‘(◡𝑈‘𝐾)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(◡𝑈‘𝐾)) | 
| 66 |  | fz0ssnn0 13663 | . . . . . . . . . . . 12
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 | 
| 67 | 66, 38 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℕ0) | 
| 68 |  | nn0fz0 13666 | . . . . . . . . . . 11
⊢ (𝐸 ∈ ℕ0
↔ 𝐸 ∈ (0...𝐸)) | 
| 69 | 67, 68 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ (0...𝐸)) | 
| 70 | 12, 69, 38, 15, 45 | splfv1 14794 | . . . . . . . . 9
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(◡𝑈‘𝐾)) = (𝑊‘(◡𝑈‘𝐾))) | 
| 71 | 65, 70 | eqtrid 2788 | . . . . . . . 8
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = (𝑊‘(◡𝑈‘𝐾))) | 
| 72 | 48, 56 | mpdan 687 | . . . . . . . 8
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) | 
| 73 | 71, 72 | eqtr3d 2778 | . . . . . . 7
⊢ (𝜑 → (𝑊‘(◡𝑈‘𝐾)) = 𝐾) | 
| 74 | 73 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → (◡𝑊‘(𝑊‘(◡𝑈‘𝐾))) = (◡𝑊‘𝐾)) | 
| 75 | 64, 74 | eqtr3d 2778 | . . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) = (◡𝑊‘𝐾)) | 
| 76 | 75 | oveq1d 7447 | . . . 4
⊢ (𝜑 → ((◡𝑈‘𝐾) + 1) = ((◡𝑊‘𝐾) + 1)) | 
| 77 | 76 | fveq2d 6909 | . . 3
⊢ (𝜑 → (𝑈‘((◡𝑈‘𝐾) + 1)) = (𝑈‘((◡𝑊‘𝐾) + 1))) | 
| 78 | 47, 58, 77 | 3eqtr3d 2784 | . 2
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = (𝑈‘((◡𝑊‘𝐾) + 1))) | 
| 79 | 3 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)) | 
| 80 | 79 | fveq1d 6907 | . . . 4
⊢ (𝜑 → (𝑈‘((◡𝑊‘𝐾) + 1)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((◡𝑊‘𝐾) + 1))) | 
| 81 | 38 | elfzelzd 13566 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℤ) | 
| 82 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) | 
| 83 | 20 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 = ((◡𝑊‘𝐽) + 1)) | 
| 84 | 83 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 − 1) = (((◡𝑊‘𝐽) + 1) − 1)) | 
| 85 |  | elfzonn0 13748 | . . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → (◡𝑊‘𝐽) ∈
ℕ0) | 
| 86 | 35, 85 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑊‘𝐽) ∈
ℕ0) | 
| 87 | 86 | nn0cnd 12591 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ ℂ) | 
| 88 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) | 
| 89 | 87, 88 | pncand 11622 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((◡𝑊‘𝐽) + 1) − 1) = (◡𝑊‘𝐽)) | 
| 90 | 84, 89 | eqtr2d 2777 | . . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑊‘𝐽) = (𝐸 − 1)) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑊‘𝐽) = (𝐸 − 1)) | 
| 92 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) = (𝐸 − 1)) | 
| 93 | 75 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) = (◡𝑊‘𝐾)) | 
| 94 | 91, 92, 93 | 3eqtr2rd 2783 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑊‘𝐾) = (◡𝑊‘𝐽)) | 
| 95 | 94 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐾)) = (𝑊‘(◡𝑊‘𝐽))) | 
| 96 |  | f1ocnvfv2 7298 | . . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐾 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) | 
| 97 | 60, 48, 96 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) | 
| 98 | 97 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐾)) = 𝐾) | 
| 99 |  | f1ocnvfv2 7298 | . . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐽 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) | 
| 100 | 60, 19, 99 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) | 
| 101 | 100 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) | 
| 102 | 95, 98, 101 | 3eqtr3d 2784 | . . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → 𝐾 = 𝐽) | 
| 103 |  | cycpmco2lem7.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≠ 𝐽) | 
| 104 | 103 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → 𝐾 ≠ 𝐽) | 
| 105 | 102, 104 | pm2.21ddne 3025 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝑈‘𝐾) = (𝐸 − 1)) → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) | 
| 106 |  | 0zd 12627 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) | 
| 107 |  | nn0p1nn 12567 | . . . . . . . . . . . . . 14
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) | 
| 108 | 86, 107 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) | 
| 109 | 20, 108 | eqeltrid 2844 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℕ) | 
| 110 |  | 0p1e1 12389 | . . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 | 
| 111 | 110 | fveq2i 6908 | . . . . . . . . . . . . 13
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) | 
| 112 |  | nnuz 12922 | . . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) | 
| 113 | 111, 112 | eqtr4i 2767 | . . . . . . . . . . . 12
⊢
(ℤ≥‘(0 + 1)) = ℕ | 
| 114 | 109, 113 | eleqtrrdi 2851 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ (ℤ≥‘(0 +
1))) | 
| 115 |  | fzosplitsnm1 13780 | . . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝐸
∈ (ℤ≥‘(0 + 1))) → (0..^𝐸) = ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) | 
| 116 | 106, 114,
115 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (0..^𝐸) = ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) | 
| 117 | 45, 116 | eleqtrd 2842 | . . . . . . . . 9
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ ((0..^(𝐸 − 1)) ∪ {(𝐸 − 1)})) | 
| 118 |  | fvex 6918 | . . . . . . . . . 10
⊢ (◡𝑈‘𝐾) ∈ V | 
| 119 |  | elunsn 4682 | . . . . . . . . . 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 218 | . . . . . . . 8
⊢ (𝜑 → ((◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1)) ∨ (◡𝑈‘𝐾) = (𝐸 − 1))) | 
| 122 | 82, 105, 121 | mpjaodan 960 | . . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) | 
| 123 |  | elfzom1elp1fzo 13772 | . . . . . . 7
⊢ ((𝐸 ∈ ℤ ∧ (◡𝑈‘𝐾) ∈ (0..^(𝐸 − 1))) → ((◡𝑈‘𝐾) + 1) ∈ (0..^𝐸)) | 
| 124 | 81, 122, 123 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((◡𝑈‘𝐾) + 1) ∈ (0..^𝐸)) | 
| 125 | 76, 124 | eqeltrrd 2841 | . . . . 5
⊢ (𝜑 → ((◡𝑊‘𝐾) + 1) ∈ (0..^𝐸)) | 
| 126 | 12, 69, 38, 15, 125 | splfv1 14794 | . . . 4
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((◡𝑊‘𝐾) + 1)) = (𝑊‘((◡𝑊‘𝐾) + 1))) | 
| 127 | 80, 126 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝑈‘((◡𝑊‘𝐾) + 1)) = (𝑊‘((◡𝑊‘𝐾) + 1))) | 
| 128 |  | 1zzd 12650 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) | 
| 129 | 81, 128 | zsubcld 12729 | . . . . . . . 8
⊢ (𝜑 → (𝐸 − 1) ∈ ℤ) | 
| 130 |  | lencl 14572 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) | 
| 131 |  | nn0fz0 13666 | . . . . . . . . . . . 12
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) | 
| 132 | 131 | biimpi 216 | . . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) | 
| 133 | 12, 130, 132 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) | 
| 134 | 133 | elfzelzd 13566 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) | 
| 135 | 134, 128 | zsubcld 12729 | . . . . . . . 8
⊢ (𝜑 → ((♯‘𝑊) − 1) ∈
ℤ) | 
| 136 | 109 | nnred 12282 | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 137 | 134 | zred 12724 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) | 
| 138 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) | 
| 139 |  | elfzle2 13569 | . . . . . . . . . 10
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ 𝐸 ≤
(♯‘𝑊)) | 
| 140 | 38, 139 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ≤ (♯‘𝑊)) | 
| 141 | 136, 137,
138, 140 | lesub1dd 11880 | . . . . . . . 8
⊢ (𝜑 → (𝐸 − 1) ≤ ((♯‘𝑊) − 1)) | 
| 142 |  | eluz 12893 | . . . . . . . . 9
⊢ (((𝐸 − 1) ∈ ℤ ∧
((♯‘𝑊) −
1) ∈ ℤ) → (((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1)) ↔ (𝐸 − 1) ≤ ((♯‘𝑊) − 1))) | 
| 143 | 142 | biimpar 477 | . . . . . . . 8
⊢ ((((𝐸 − 1) ∈ ℤ ∧
((♯‘𝑊) −
1) ∈ ℤ) ∧ (𝐸
− 1) ≤ ((♯‘𝑊) − 1)) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1))) | 
| 144 | 129, 135,
141, 143 | syl21anc 837 | . . . . . . 7
⊢ (𝜑 → ((♯‘𝑊) − 1) ∈
(ℤ≥‘(𝐸 − 1))) | 
| 145 |  | fzoss2 13728 | . . . . . . 7
⊢
(((♯‘𝑊)
− 1) ∈ (ℤ≥‘(𝐸 − 1)) → (0..^(𝐸 − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) | 
| 146 | 144, 145 | syl 17 | . . . . . 6
⊢ (𝜑 → (0..^(𝐸 − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) | 
| 147 | 146, 122 | sseldd 3983 | . . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^((♯‘𝑊) − 1))) | 
| 148 | 75, 147 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (◡𝑊‘𝐾) ∈ (0..^((♯‘𝑊) − 1))) | 
| 149 | 1, 2, 12, 28, 148 | cycpmfv1 33134 | . . 3
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐾))) = (𝑊‘((◡𝑊‘𝐾) + 1))) | 
| 150 | 97 | fveq2d 6909 | . . 3
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘(◡𝑊‘𝐾))) = ((𝑀‘𝑊)‘𝐾)) | 
| 151 | 127, 149,
150 | 3eqtr2rd 2783 | . 2
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐾) = (𝑈‘((◡𝑊‘𝐾) + 1))) | 
| 152 | 78, 151 | eqtr4d 2779 | 1
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾)) |