| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cycpmco2.1 | . . . . 5
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) | 
| 2 |  | cycpmco2.w | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) | 
| 3 |  | cycpmco2.e | . . . . . . 7
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) | 
| 4 |  | ovexd 7467 | . . . . . . 7
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) | 
| 5 | 3, 4 | eqeltrid 2844 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ V) | 
| 6 |  | cycpmco2.i | . . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) | 
| 7 | 6 | eldifad 3962 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝐷) | 
| 8 | 7 | s1cld 14642 | . . . . . 6
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) | 
| 9 |  | splval 14790 | . . . . . 6
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 10 | 2, 5, 5, 8, 9 | syl13anc 1373 | . . . . 5
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 11 | 1, 10 | eqtrid 2788 | . . . 4
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) | 
| 12 | 11 | fveq1d 6907 | . . 3
⊢ (𝜑 → (𝑈‘𝐸) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘𝐸)) | 
| 13 |  | ssrab2 4079 | . . . . . . 7
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 | 
| 14 |  | cycpmco2.d | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 15 |  | cycpmco2.c | . . . . . . . . . . 11
⊢ 𝑀 = (toCyc‘𝐷) | 
| 16 |  | cycpmco2.s | . . . . . . . . . . 11
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 17 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 18 | 15, 16, 17 | tocycf 33138 | . . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) | 
| 19 | 14, 18 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) | 
| 20 | 19 | fdmd 6745 | . . . . . . . 8
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 21 | 2, 20 | eleqtrd 2842 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 22 | 13, 21 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) | 
| 23 |  | pfxcl 14716 | . . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) | 
| 24 | 22, 23 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) | 
| 25 |  | ccatcl 14613 | . . . . 5
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) | 
| 26 | 24, 8, 25 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) | 
| 27 |  | swrdcl 14684 | . . . . 5
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) | 
| 28 | 22, 27 | syl 17 | . . . 4
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) | 
| 29 |  | fz0ssnn0 13663 | . . . . . . 7
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 | 
| 30 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | 
| 31 |  | dmeq 5913 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) | 
| 32 |  | eqidd 2737 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) | 
| 33 | 30, 31, 32 | f1eq123d 6839 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 34 | 33 | elrab 3691 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 35 | 21, 34 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 36 | 35 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) | 
| 37 |  | f1cnv 6871 | . . . . . . . . . . . 12
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) | 
| 38 |  | f1of 6847 | . . . . . . . . . . . 12
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 39 | 36, 37, 38 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) | 
| 40 |  | cycpmco2.j | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) | 
| 41 | 39, 40 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) | 
| 42 |  | wrddm 14560 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 43 | 22, 42 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 44 | 41, 43 | eleqtrd 2842 | . . . . . . . . 9
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) | 
| 45 |  | fzofzp1 13804 | . . . . . . . . 9
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 46 | 44, 45 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) | 
| 47 | 3, 46 | eqeltrid 2844 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) | 
| 48 | 29, 47 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℕ0) | 
| 49 |  | fzonn0p1 13782 | . . . . . 6
⊢ (𝐸 ∈ ℕ0
→ 𝐸 ∈ (0..^(𝐸 + 1))) | 
| 50 | 48, 49 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ (0..^(𝐸 + 1))) | 
| 51 |  | ccatws1len 14659 | . . . . . . . 8
⊢ ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) | 
| 52 | 22, 23, 51 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) | 
| 53 |  | pfxlen 14722 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸) | 
| 54 | 22, 47, 53 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸) | 
| 55 | 54 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1)) | 
| 56 | 52, 55 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) | 
| 57 | 56 | oveq2d 7448 | . . . . 5
⊢ (𝜑 →
(0..^(♯‘((𝑊
prefix 𝐸) ++
〈“𝐼”〉))) = (0..^(𝐸 + 1))) | 
| 58 | 50, 57 | eleqtrrd 2843 | . . . 4
⊢ (𝜑 → 𝐸 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) | 
| 59 |  | ccatval1 14616 | . . . 4
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷 ∧ 𝐸 ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘𝐸) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘𝐸)) | 
| 60 | 26, 28, 58, 59 | syl3anc 1372 | . . 3
⊢ (𝜑 → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘𝐸) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘𝐸)) | 
| 61 | 48 | nn0zd 12641 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℤ) | 
| 62 |  | elfzomin 13777 | . . . . . 6
⊢ (𝐸 ∈ ℤ → 𝐸 ∈ (𝐸..^(𝐸 + 1))) | 
| 63 | 61, 62 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ (𝐸..^(𝐸 + 1))) | 
| 64 |  | s1len 14645 | . . . . . . . 8
⊢
(♯‘〈“𝐼”〉) = 1 | 
| 65 | 64 | a1i 11 | . . . . . . 7
⊢ (𝜑 →
(♯‘〈“𝐼”〉) = 1) | 
| 66 | 54, 65 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + (♯‘〈“𝐼”〉)) = (𝐸 + 1)) | 
| 67 | 54, 66 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸))..^((♯‘(𝑊 prefix 𝐸)) + (♯‘〈“𝐼”〉))) = (𝐸..^(𝐸 + 1))) | 
| 68 | 63, 67 | eleqtrrd 2843 | . . . 4
⊢ (𝜑 → 𝐸 ∈ ((♯‘(𝑊 prefix 𝐸))..^((♯‘(𝑊 prefix 𝐸)) + (♯‘〈“𝐼”〉)))) | 
| 69 |  | ccatval2 14617 | . . . 4
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷 ∧ 𝐸 ∈ ((♯‘(𝑊 prefix 𝐸))..^((♯‘(𝑊 prefix 𝐸)) + (♯‘〈“𝐼”〉)))) →
(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘𝐸) = (〈“𝐼”〉‘(𝐸 − (♯‘(𝑊 prefix 𝐸))))) | 
| 70 | 24, 8, 68, 69 | syl3anc 1372 | . . 3
⊢ (𝜑 → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘𝐸) = (〈“𝐼”〉‘(𝐸 − (♯‘(𝑊 prefix 𝐸))))) | 
| 71 | 12, 60, 70 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (𝑈‘𝐸) = (〈“𝐼”〉‘(𝐸 − (♯‘(𝑊 prefix 𝐸))))) | 
| 72 | 54 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (𝐸 − (♯‘(𝑊 prefix 𝐸))) = (𝐸 − 𝐸)) | 
| 73 | 48 | nn0cnd 12591 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 74 | 73 | subidd 11609 | . . . 4
⊢ (𝜑 → (𝐸 − 𝐸) = 0) | 
| 75 | 72, 74 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝐸 − (♯‘(𝑊 prefix 𝐸))) = 0) | 
| 76 | 75 | fveq2d 6909 | . 2
⊢ (𝜑 → (〈“𝐼”〉‘(𝐸 − (♯‘(𝑊 prefix 𝐸)))) = (〈“𝐼”〉‘0)) | 
| 77 |  | s1fv 14649 | . . 3
⊢ (𝐼 ∈ (𝐷 ∖ ran 𝑊) → (〈“𝐼”〉‘0) = 𝐼) | 
| 78 | 6, 77 | syl 17 | . 2
⊢ (𝜑 → (〈“𝐼”〉‘0) = 𝐼) | 
| 79 | 71, 76, 78 | 3eqtrd 2780 | 1
⊢ (𝜑 → (𝑈‘𝐸) = 𝐼) |