| 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 |  | fz0ssnn0 13663 | . . . . . . . 8
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 | 
| 23 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | 
| 24 |  | dmeq 5913 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) | 
| 25 |  | eqidd 2737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) | 
| 26 | 23, 24, 25 | f1eq123d 6839 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 27 | 26 | elrab 3691 | . . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 28 | 11, 27 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 29 | 28 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) | 
| 30 |  | f1cnv 6871 | . . . . . . . . . . . . 13
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) | 
| 31 |  | f1of 6847 | . . . . . . . . . . . . 13
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 32 | 29, 30, 31 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 33 | 32, 19 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) | 
| 34 |  | wrddm 14560 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 35 | 12, 34 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 36 | 33, 35 | eleqtrd 2842 | . . . . . . . . . 10
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) | 
| 37 |  | fzofzp1 13804 | . . . . . . . . . 10
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 39 | 20, 38 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) | 
| 40 | 22, 39 | sselid 3980 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℕ0) | 
| 41 |  | nn0uz 12921 | . . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) | 
| 42 | 40, 41 | eleqtrdi 2850 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈
(ℤ≥‘0)) | 
| 43 |  | fzoss1 13727 | . . . . . 6
⊢ (𝐸 ∈
(ℤ≥‘0) → (𝐸..^((♯‘𝑈) − 1)) ⊆
(0..^((♯‘𝑈)
− 1))) | 
| 44 | 42, 43 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐸..^((♯‘𝑈) − 1)) ⊆
(0..^((♯‘𝑈)
− 1))) | 
| 45 |  | cycpmco2lem6.1 | . . . . 5
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1))) | 
| 46 | 44, 45 | sseldd 3983 | . . . 4
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^((♯‘𝑈) − 1))) | 
| 47 | 1, 2, 18, 21, 46 | cycpmfv1 33134 | . . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = (𝑈‘((◡𝑈‘𝐾) + 1))) | 
| 48 |  | cycpmco2lem.1 | . . . . 5
⊢ (𝜑 → 𝐾 ∈ 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 | 48, 56 | mpdan 687 | . . . 4
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = 𝐾) | 
| 58 | 57 | fveq2d 6909 | . . 3
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑈‘𝐾))) = ((𝑀‘𝑈)‘𝐾)) | 
| 59 | 3 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)) | 
| 60 |  | fzossz 13720 | . . . . . . . 8
⊢ (𝐸..^((♯‘𝑈) − 1)) ⊆
ℤ | 
| 61 | 60, 45 | sselid 3980 | . . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ ℤ) | 
| 62 | 61 | zcnd 12725 | . . . . . 6
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ ℂ) | 
| 63 | 40 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 64 |  | 1cnd 11257 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) | 
| 65 | 62, 63, 64 | nppcan3d 11648 | . . . . 5
⊢ (𝜑 → (((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸)) = ((◡𝑈‘𝐾) + 1)) | 
| 66 | 65 | eqcomd 2742 | . . . 4
⊢ (𝜑 → ((◡𝑈‘𝐾) + 1) = (((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸))) | 
| 67 | 59, 66 | fveq12d 6912 | . . 3
⊢ (𝜑 → (𝑈‘((◡𝑈‘𝐾) + 1)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸)))) | 
| 68 | 47, 58, 67 | 3eqtr3d 2784 | . 2
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸)))) | 
| 69 | 62, 63 | npcand 11625 | . . . 4
⊢ (𝜑 → (((◡𝑈‘𝐾) − 𝐸) + 𝐸) = (◡𝑈‘𝐾)) | 
| 70 | 69 | fveq2d 6909 | . . 3
⊢ (𝜑 → (𝑊‘(((◡𝑈‘𝐾) − 𝐸) + 𝐸)) = (𝑊‘(◡𝑈‘𝐾))) | 
| 71 |  | nn0fz0 13666 | . . . . 5
⊢ (𝐸 ∈ ℕ0
↔ 𝐸 ∈ (0...𝐸)) | 
| 72 | 40, 71 | sylib 218 | . . . 4
⊢ (𝜑 → 𝐸 ∈ (0...𝐸)) | 
| 73 |  | lencl 14572 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) | 
| 74 | 12, 73 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) | 
| 75 | 74 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℂ) | 
| 76 |  | ovexd 7467 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) | 
| 77 | 20, 76 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ V) | 
| 78 |  | splval 14790 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 79 | 5, 77, 77, 15, 78 | syl13anc 1373 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 80 | 3, 79 | eqtrid 2788 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 81 | 80 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) | 
| 82 |  | pfxcl 14716 | . . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) | 
| 83 | 12, 82 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) | 
| 84 |  | ccatcl 14613 | . . . . . . . . . . . . . 14
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) | 
| 85 | 83, 15, 84 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) | 
| 86 |  | swrdcl 14684 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) | 
| 87 | 12, 86 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) | 
| 88 |  | ccatlen 14614 | . . . . . . . . . . . . 13
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) | 
| 89 | 85, 87, 88 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) | 
| 90 |  | ccatws1len 14659 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) | 
| 91 | 12, 82, 90 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) | 
| 92 |  | pfxlen 14722 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸) | 
| 93 | 12, 39, 92 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸) | 
| 94 | 93 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1)) | 
| 95 | 91, 94 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) | 
| 96 |  | nn0fz0 13666 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) | 
| 97 | 74, 96 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) | 
| 98 |  | swrdlen 14686 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈𝐸,
(♯‘𝑊)〉)) =
((♯‘𝑊) −
𝐸)) | 
| 99 | 12, 39, 97, 98 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐸)) | 
| 100 | 95, 99 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) | 
| 101 | 81, 89, 100 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) | 
| 102 | 40 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℤ) | 
| 103 | 102 | peano2zd 12727 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 + 1) ∈ ℤ) | 
| 104 | 103 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 + 1) ∈ ℂ) | 
| 105 | 104, 75, 63 | addsubassd 11641 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) | 
| 106 | 63, 64, 75 | addassd 11284 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊)))) | 
| 107 | 106 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) | 
| 108 | 101, 105,
107 | 3eqtr2d 2782 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) | 
| 109 | 64, 75 | addcld 11281 | . . . . . . . . . . 11
⊢ (𝜑 → (1 + (♯‘𝑊)) ∈
ℂ) | 
| 110 | 63, 109 | pncan2d 11623 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊))) | 
| 111 | 64, 75 | addcomd 11464 | . . . . . . . . . 10
⊢ (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1)) | 
| 112 | 108, 110,
111 | 3eqtrd 2780 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1)) | 
| 113 | 75, 64, 112 | mvrraddd 11676 | . . . . . . . 8
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) | 
| 114 | 113 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (𝐸..^((♯‘𝑈) − 1)) = (𝐸..^(♯‘𝑊))) | 
| 115 | 45, 114 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^(♯‘𝑊))) | 
| 116 |  | fzosubel 13764 | . . . . . 6
⊢ (((◡𝑈‘𝐾) ∈ (𝐸..^(♯‘𝑊)) ∧ 𝐸 ∈ ℤ) → ((◡𝑈‘𝐾) − 𝐸) ∈ ((𝐸 − 𝐸)..^((♯‘𝑊) − 𝐸))) | 
| 117 | 115, 102,
116 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((◡𝑈‘𝐾) − 𝐸) ∈ ((𝐸 − 𝐸)..^((♯‘𝑊) − 𝐸))) | 
| 118 | 63 | subidd 11609 | . . . . . 6
⊢ (𝜑 → (𝐸 − 𝐸) = 0) | 
| 119 | 118 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((𝐸 − 𝐸)..^((♯‘𝑊) − 𝐸)) = (0..^((♯‘𝑊) − 𝐸))) | 
| 120 | 117, 119 | eleqtrd 2842 | . . . 4
⊢ (𝜑 → ((◡𝑈‘𝐾) − 𝐸) ∈ (0..^((♯‘𝑊) − 𝐸))) | 
| 121 | 64, 63 | addcomd 11464 | . . . . 5
⊢ (𝜑 → (1 + 𝐸) = (𝐸 + 1)) | 
| 122 |  | s1len 14645 | . . . . . 6
⊢
(♯‘〈“𝐼”〉) = 1 | 
| 123 | 122 | oveq2i 7443 | . . . . 5
⊢ (𝐸 +
(♯‘〈“𝐼”〉)) = (𝐸 + 1) | 
| 124 | 121, 123 | eqtr4di 2794 | . . . 4
⊢ (𝜑 → (1 + 𝐸) = (𝐸 + (♯‘〈“𝐼”〉))) | 
| 125 | 12, 72, 39, 15, 120, 124 | splfv3 32944 | . . 3
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸))) = (𝑊‘(((◡𝑈‘𝐾) − 𝐸) + 𝐸))) | 
| 126 | 113 | oveq1d 7447 | . . . . . . . 8
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) =
((♯‘𝑊) −
1)) | 
| 127 | 126 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (𝐸..^(((♯‘𝑈) − 1) − 1)) = (𝐸..^((♯‘𝑊) − 1))) | 
| 128 |  | fzoss1 13727 | . . . . . . . 8
⊢ (𝐸 ∈
(ℤ≥‘0) → (𝐸..^((♯‘𝑊) − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) | 
| 129 | 42, 128 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐸..^((♯‘𝑊) − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) | 
| 130 | 127, 129 | eqsstrd 4017 | . . . . . 6
⊢ (𝜑 → (𝐸..^(((♯‘𝑈) − 1) − 1)) ⊆
(0..^((♯‘𝑊)
− 1))) | 
| 131 |  | f1ocnvdm 7306 | . . . . . . . . . 10
⊢ ((𝑈:dom 𝑈–1-1-onto→ran
𝑈 ∧ 𝐾 ∈ ran 𝑈) → (◡𝑈‘𝐾) ∈ dom 𝑈) | 
| 132 | 50, 54, 131 | syl2an2r 685 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ ran 𝑊) → (◡𝑈‘𝐾) ∈ dom 𝑈) | 
| 133 | 48, 132 | mpdan 687 | . . . . . . . 8
⊢ (𝜑 → (◡𝑈‘𝐾) ∈ dom 𝑈) | 
| 134 | 74 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) | 
| 135 | 134 | peano2zd 12727 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝑊) + 1) ∈
ℤ) | 
| 136 |  | elfzonn0 13748 | . . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → (◡𝑊‘𝐽) ∈
ℕ0) | 
| 137 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) | 
| 138 | 36, 136, 137 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ ℕ) | 
| 139 | 20, 138 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ ℕ) | 
| 140 | 139 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 141 | 134 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) | 
| 142 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) | 
| 143 |  | elfzle2 13569 | . . . . . . . . . . . . . . 15
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ 𝐸 ≤
(♯‘𝑊)) | 
| 144 | 39, 143 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ≤ (♯‘𝑊)) | 
| 145 | 140, 141,
142, 144 | leadd1dd 11878 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 + 1) ≤ ((♯‘𝑊) + 1)) | 
| 146 |  | eluz2 12885 | . . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
+ 1) ∈ (ℤ≥‘(𝐸 + 1)) ↔ ((𝐸 + 1) ∈ ℤ ∧
((♯‘𝑊) + 1)
∈ ℤ ∧ (𝐸 +
1) ≤ ((♯‘𝑊)
+ 1))) | 
| 147 | 103, 135,
145, 146 | syl3anbrc 1343 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝑊) + 1) ∈
(ℤ≥‘(𝐸 + 1))) | 
| 148 |  | fzoss2 13728 | . . . . . . . . . . . 12
⊢
(((♯‘𝑊)
+ 1) ∈ (ℤ≥‘(𝐸 + 1)) → (0..^(𝐸 + 1)) ⊆ (0..^((♯‘𝑊) + 1))) | 
| 149 | 147, 148 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (0..^(𝐸 + 1)) ⊆ (0..^((♯‘𝑊) + 1))) | 
| 150 |  | fzonn0p1 13782 | . . . . . . . . . . . 12
⊢ (𝐸 ∈ ℕ0
→ 𝐸 ∈ (0..^(𝐸 + 1))) | 
| 151 | 40, 150 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ (0..^(𝐸 + 1))) | 
| 152 | 149, 151 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ (0..^((♯‘𝑊) + 1))) | 
| 153 | 112 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝜑 → (0..^(♯‘𝑈)) = (0..^((♯‘𝑊) + 1))) | 
| 154 | 152, 153 | eleqtrrd 2843 | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ (0..^(♯‘𝑈))) | 
| 155 |  | wrddm 14560 | . . . . . . . . . 10
⊢ (𝑈 ∈ Word 𝐷 → dom 𝑈 = (0..^(♯‘𝑈))) | 
| 156 | 18, 155 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → dom 𝑈 = (0..^(♯‘𝑈))) | 
| 157 | 154, 156 | eleqtrrd 2843 | . . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ dom 𝑈) | 
| 158 |  | cycpmco2lem6.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ≠ 𝐼) | 
| 159 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2lem2 33148 | . . . . . . . . 9
⊢ (𝜑 → (𝑈‘𝐸) = 𝐼) | 
| 160 | 158, 57, 159 | 3netr4d 3017 | . . . . . . . 8
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) ≠ (𝑈‘𝐸)) | 
| 161 |  | f1fveq 7283 | . . . . . . . . . 10
⊢ ((𝑈:dom 𝑈–1-1→𝐷 ∧ ((◡𝑈‘𝐾) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈)) → ((𝑈‘(◡𝑈‘𝐾)) = (𝑈‘𝐸) ↔ (◡𝑈‘𝐾) = 𝐸)) | 
| 162 | 161 | necon3bid 2984 | . . . . . . . . 9
⊢ ((𝑈:dom 𝑈–1-1→𝐷 ∧ ((◡𝑈‘𝐾) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈)) → ((𝑈‘(◡𝑈‘𝐾)) ≠ (𝑈‘𝐸) ↔ (◡𝑈‘𝐾) ≠ 𝐸)) | 
| 163 | 162 | biimp3a 1470 | . . . . . . . 8
⊢ ((𝑈:dom 𝑈–1-1→𝐷 ∧ ((◡𝑈‘𝐾) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈) ∧ (𝑈‘(◡𝑈‘𝐾)) ≠ (𝑈‘𝐸)) → (◡𝑈‘𝐾) ≠ 𝐸) | 
| 164 | 21, 133, 157, 160, 163 | syl121anc 1376 | . . . . . . 7
⊢ (𝜑 → (◡𝑈‘𝐾) ≠ 𝐸) | 
| 165 |  | fzom1ne1 32804 | . . . . . . 7
⊢ (((◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1)) ∧ (◡𝑈‘𝐾) ≠ 𝐸) → ((◡𝑈‘𝐾) − 1) ∈ (𝐸..^(((♯‘𝑈) − 1) − 1))) | 
| 166 | 45, 164, 165 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((◡𝑈‘𝐾) − 1) ∈ (𝐸..^(((♯‘𝑈) − 1) − 1))) | 
| 167 | 130, 166 | sseldd 3983 | . . . . 5
⊢ (𝜑 → ((◡𝑈‘𝐾) − 1) ∈
(0..^((♯‘𝑊)
− 1))) | 
| 168 | 1, 2, 12, 29, 167 | cycpmfv1 33134 | . . . 4
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘((◡𝑈‘𝐾) − 1))) = (𝑊‘(((◡𝑈‘𝐾) − 1) + 1))) | 
| 169 | 62, 64, 63 | subsub4d 11652 | . . . . . . . . . 10
⊢ (𝜑 → (((◡𝑈‘𝐾) − 1) − 𝐸) = ((◡𝑈‘𝐾) − (1 + 𝐸))) | 
| 170 | 169 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((((◡𝑈‘𝐾) − 1) − 𝐸) + (1 + 𝐸)) = (((◡𝑈‘𝐾) − (1 + 𝐸)) + (1 + 𝐸))) | 
| 171 | 64, 63 | addcld 11281 | . . . . . . . . . 10
⊢ (𝜑 → (1 + 𝐸) ∈ ℂ) | 
| 172 | 62, 171 | npcand 11625 | . . . . . . . . 9
⊢ (𝜑 → (((◡𝑈‘𝐾) − (1 + 𝐸)) + (1 + 𝐸)) = (◡𝑈‘𝐾)) | 
| 173 | 170, 172 | eqtr2d 2777 | . . . . . . . 8
⊢ (𝜑 → (◡𝑈‘𝐾) = ((((◡𝑈‘𝐾) − 1) − 𝐸) + (1 + 𝐸))) | 
| 174 | 59, 173 | fveq12d 6912 | . . . . . . 7
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((((◡𝑈‘𝐾) − 1) − 𝐸) + (1 + 𝐸)))) | 
| 175 | 63, 75 | pncan3d 11624 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 + ((♯‘𝑊) − 𝐸)) = (♯‘𝑊)) | 
| 176 | 113, 134 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝑈) − 1) ∈
ℤ) | 
| 177 |  | 1zzd 12650 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℤ) | 
| 178 | 176, 177 | zsubcld 12729 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) ∈
ℤ) | 
| 179 | 178 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) ∈
ℝ) | 
| 180 | 113, 141 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((♯‘𝑈) − 1) ∈
ℝ) | 
| 181 | 180 | ltm1d 12201 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) <
((♯‘𝑈) −
1)) | 
| 182 | 181, 113 | breqtrd 5168 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) <
(♯‘𝑊)) | 
| 183 | 179, 141,
182 | ltled 11410 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((♯‘𝑈) − 1) − 1) ≤
(♯‘𝑊)) | 
| 184 |  | eluz1 12883 | . . . . . . . . . . . . . 14
⊢
((((♯‘𝑈)
− 1) − 1) ∈ ℤ → ((♯‘𝑊) ∈
(ℤ≥‘(((♯‘𝑈) − 1) − 1)) ↔
((♯‘𝑊) ∈
ℤ ∧ (((♯‘𝑈) − 1) − 1) ≤
(♯‘𝑊)))) | 
| 185 | 184 | biimpar 477 | . . . . . . . . . . . . 13
⊢
(((((♯‘𝑈) − 1) − 1) ∈ ℤ ∧
((♯‘𝑊) ∈
ℤ ∧ (((♯‘𝑈) − 1) − 1) ≤
(♯‘𝑊))) →
(♯‘𝑊) ∈
(ℤ≥‘(((♯‘𝑈) − 1) − 1))) | 
| 186 | 178, 134,
183, 185 | syl12anc 836 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑊) ∈
(ℤ≥‘(((♯‘𝑈) − 1) − 1))) | 
| 187 | 175, 186 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 + ((♯‘𝑊) − 𝐸)) ∈
(ℤ≥‘(((♯‘𝑈) − 1) − 1))) | 
| 188 |  | fzoss2 13728 | . . . . . . . . . . 11
⊢ ((𝐸 + ((♯‘𝑊) − 𝐸)) ∈
(ℤ≥‘(((♯‘𝑈) − 1) − 1)) → (𝐸..^(((♯‘𝑈) − 1) − 1)) ⊆
(𝐸..^(𝐸 + ((♯‘𝑊) − 𝐸)))) | 
| 189 | 187, 188 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸..^(((♯‘𝑈) − 1) − 1)) ⊆ (𝐸..^(𝐸 + ((♯‘𝑊) − 𝐸)))) | 
| 190 | 189, 166 | sseldd 3983 | . . . . . . . . 9
⊢ (𝜑 → ((◡𝑈‘𝐾) − 1) ∈ (𝐸..^(𝐸 + ((♯‘𝑊) − 𝐸)))) | 
| 191 | 134, 102 | zsubcld 12729 | . . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑊) − 𝐸) ∈ ℤ) | 
| 192 |  | fzosubel3 13766 | . . . . . . . . 9
⊢ ((((◡𝑈‘𝐾) − 1) ∈ (𝐸..^(𝐸 + ((♯‘𝑊) − 𝐸))) ∧ ((♯‘𝑊) − 𝐸) ∈ ℤ) → (((◡𝑈‘𝐾) − 1) − 𝐸) ∈ (0..^((♯‘𝑊) − 𝐸))) | 
| 193 | 190, 191,
192 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (((◡𝑈‘𝐾) − 1) − 𝐸) ∈ (0..^((♯‘𝑊) − 𝐸))) | 
| 194 | 12, 72, 39, 15, 193, 124 | splfv3 32944 | . . . . . . 7
⊢ (𝜑 → ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘((((◡𝑈‘𝐾) − 1) − 𝐸) + (1 + 𝐸))) = (𝑊‘((((◡𝑈‘𝐾) − 1) − 𝐸) + 𝐸))) | 
| 195 | 62, 64 | subcld 11621 | . . . . . . . . 9
⊢ (𝜑 → ((◡𝑈‘𝐾) − 1) ∈
ℂ) | 
| 196 | 195, 63 | npcand 11625 | . . . . . . . 8
⊢ (𝜑 → ((((◡𝑈‘𝐾) − 1) − 𝐸) + 𝐸) = ((◡𝑈‘𝐾) − 1)) | 
| 197 | 196 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → (𝑊‘((((◡𝑈‘𝐾) − 1) − 𝐸) + 𝐸)) = (𝑊‘((◡𝑈‘𝐾) − 1))) | 
| 198 | 174, 194,
197 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → (𝑈‘(◡𝑈‘𝐾)) = (𝑊‘((◡𝑈‘𝐾) − 1))) | 
| 199 | 198, 57 | eqtr3d 2778 | . . . . 5
⊢ (𝜑 → (𝑊‘((◡𝑈‘𝐾) − 1)) = 𝐾) | 
| 200 | 199 | fveq2d 6909 | . . . 4
⊢ (𝜑 → ((𝑀‘𝑊)‘(𝑊‘((◡𝑈‘𝐾) − 1))) = ((𝑀‘𝑊)‘𝐾)) | 
| 201 | 62, 64 | npcand 11625 | . . . . 5
⊢ (𝜑 → (((◡𝑈‘𝐾) − 1) + 1) = (◡𝑈‘𝐾)) | 
| 202 | 201 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝑊‘(((◡𝑈‘𝐾) − 1) + 1)) = (𝑊‘(◡𝑈‘𝐾))) | 
| 203 | 168, 200,
202 | 3eqtr3d 2784 | . . 3
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐾) = (𝑊‘(◡𝑈‘𝐾))) | 
| 204 | 70, 125, 203 | 3eqtr4rd 2787 | . 2
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐾) = ((𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉)‘(((◡𝑈‘𝐾) − 𝐸) + (1 + 𝐸)))) | 
| 205 | 68, 204 | eqtr4d 2779 | 1
⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾)) |