Proof of Theorem ccatws1f1olast
| Step | Hyp | Ref
| Expression |
| 1 | | ccatws1f1olast.1 |
. . . . . . 7
⊢ 𝑁 = (♯‘𝑊) |
| 2 | | ccatws1f1olast.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Word 𝑆) |
| 3 | | lencl 14571 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈
ℕ0) |
| 4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
| 5 | 1, 4 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 6 | | fzossfzop1 13782 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
| 8 | | sswrd 14560 |
. . . . 5
⊢
((0..^𝑁) ⊆
(0..^(𝑁 + 1)) → Word
(0..^𝑁) ⊆ Word
(0..^(𝑁 +
1))) |
| 9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → Word (0..^𝑁) ⊆ Word (0..^(𝑁 + 1))) |
| 10 | | ccatws1f1olast.5 |
. . . . . 6
⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁)) |
| 11 | | f1of 6848 |
. . . . . 6
⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁)) |
| 12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇:(0..^𝑁)⟶(0..^𝑁)) |
| 13 | | iswrdi 14556 |
. . . . 5
⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁)) |
| 14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ Word (0..^𝑁)) |
| 15 | 9, 14 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Word (0..^(𝑁 + 1))) |
| 16 | | fzonn0p1 13781 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
| 17 | 5, 16 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1))) |
| 18 | 17 | s1cld 14641 |
. . 3
⊢ (𝜑 → 〈“𝑁”〉 ∈ Word
(0..^(𝑁 +
1))) |
| 19 | 1 | oveq1i 7441 |
. . . . 5
⊢ (𝑁 + 1) = ((♯‘𝑊) + 1) |
| 20 | | ccatws1len 14658 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑆 → (♯‘(𝑊 ++ 〈“𝑋”〉)) = ((♯‘𝑊) + 1)) |
| 21 | 2, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑊 ++ 〈“𝑋”〉)) =
((♯‘𝑊) +
1)) |
| 22 | 19, 21 | eqtr4id 2796 |
. . . 4
⊢ (𝜑 → (𝑁 + 1) = (♯‘(𝑊 ++ 〈“𝑋”〉))) |
| 23 | | ccatws1f1olast.4 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
| 24 | | ccatws1cl 14654 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆) → (𝑊 ++ 〈“𝑋”〉) ∈ Word 𝑆) |
| 25 | 2, 23, 24 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑊 ++ 〈“𝑋”〉) ∈ Word 𝑆) |
| 26 | 22, 25 | wrdfd 32918 |
. . 3
⊢ (𝜑 → (𝑊 ++ 〈“𝑋”〉):(0..^(𝑁 + 1))⟶𝑆) |
| 27 | | ccatco 14874 |
. . 3
⊢ ((𝑇 ∈ Word (0..^(𝑁 + 1)) ∧ 〈“𝑁”〉 ∈ Word
(0..^(𝑁 + 1)) ∧ (𝑊 ++ 〈“𝑋”〉):(0..^(𝑁 + 1))⟶𝑆) → ((𝑊 ++ 〈“𝑋”〉) ∘ (𝑇 ++ 〈“𝑁”〉)) = (((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇) ++ ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉))) |
| 28 | 15, 18, 26, 27 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ (𝑇 ++ 〈“𝑁”〉)) = (((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇) ++ ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉))) |
| 29 | 12 | frnd 6744 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ⊆ (0..^𝑁)) |
| 30 | | cores 6269 |
. . . . 5
⊢ (ran
𝑇 ⊆ (0..^𝑁) → (((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁)) ∘ 𝑇) = ((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇)) |
| 31 | 29, 30 | syl 17 |
. . . 4
⊢ (𝜑 → (((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁)) ∘ 𝑇) = ((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇)) |
| 32 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑁 = (♯‘𝑊)) |
| 33 | 32 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) prefix 𝑁) = ((𝑊 ++ 〈“𝑋”〉) prefix (♯‘𝑊))) |
| 34 | | fzossfz 13718 |
. . . . . . . . . 10
⊢
(0..^(𝑁 + 1))
⊆ (0...(𝑁 +
1)) |
| 35 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) = ((♯‘𝑊) + 1)) |
| 36 | 35 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝑁 + 1)) = (0...((♯‘𝑊) + 1))) |
| 37 | 34, 36 | sseqtrid 4026 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(𝑁 + 1)) ⊆ (0...((♯‘𝑊) + 1))) |
| 38 | 37, 17 | sseldd 3984 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (0...((♯‘𝑊) + 1))) |
| 39 | 21 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (0...(♯‘(𝑊 ++ 〈“𝑋”〉))) =
(0...((♯‘𝑊) +
1))) |
| 40 | 38, 39 | eleqtrrd 2844 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (0...(♯‘(𝑊 ++ 〈“𝑋”〉)))) |
| 41 | | pfxres 14717 |
. . . . . . 7
⊢ (((𝑊 ++ 〈“𝑋”〉) ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(♯‘(𝑊 ++ 〈“𝑋”〉)))) → ((𝑊 ++ 〈“𝑋”〉) prefix 𝑁) = ((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁))) |
| 42 | 25, 40, 41 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) prefix 𝑁) = ((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁))) |
| 43 | 23 | s1cld 14641 |
. . . . . . 7
⊢ (𝜑 → 〈“𝑋”〉 ∈ Word 𝑆) |
| 44 | | pfxccat1 14740 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑆 ∧ 〈“𝑋”〉 ∈ Word 𝑆) → ((𝑊 ++ 〈“𝑋”〉) prefix (♯‘𝑊)) = 𝑊) |
| 45 | 2, 43, 44 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) prefix (♯‘𝑊)) = 𝑊) |
| 46 | 33, 42, 45 | 3eqtr3d 2785 |
. . . . 5
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁)) = 𝑊) |
| 47 | 46 | coeq1d 5872 |
. . . 4
⊢ (𝜑 → (((𝑊 ++ 〈“𝑋”〉) ↾ (0..^𝑁)) ∘ 𝑇) = (𝑊 ∘ 𝑇)) |
| 48 | 31, 47 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇) = (𝑊 ∘ 𝑇)) |
| 49 | | s1co 14872 |
. . . . 5
⊢ ((𝑁 ∈ (0..^(𝑁 + 1)) ∧ (𝑊 ++ 〈“𝑋”〉):(0..^(𝑁 + 1))⟶𝑆) → ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉) =
〈“((𝑊 ++
〈“𝑋”〉)‘𝑁)”〉) |
| 50 | 17, 26, 49 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉) =
〈“((𝑊 ++
〈“𝑋”〉)‘𝑁)”〉) |
| 51 | | ccats1val2 14665 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆 ∧ 𝑁 = (♯‘𝑊)) → ((𝑊 ++ 〈“𝑋”〉)‘𝑁) = 𝑋) |
| 52 | 2, 23, 32, 51 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉)‘𝑁) = 𝑋) |
| 53 | 52 | s1eqd 14639 |
. . . 4
⊢ (𝜑 → 〈“((𝑊 ++ 〈“𝑋”〉)‘𝑁)”〉 =
〈“𝑋”〉) |
| 54 | 50, 53 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉) =
〈“𝑋”〉) |
| 55 | 48, 54 | oveq12d 7449 |
. 2
⊢ (𝜑 → (((𝑊 ++ 〈“𝑋”〉) ∘ 𝑇) ++ ((𝑊 ++ 〈“𝑋”〉) ∘ 〈“𝑁”〉)) = ((𝑊 ∘ 𝑇) ++ 〈“𝑋”〉)) |
| 56 | 28, 55 | eqtrd 2777 |
1
⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ (𝑇 ++ 〈“𝑁”〉)) = ((𝑊 ∘ 𝑇) ++ 〈“𝑋”〉)) |