Proof of Theorem splfv1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | spllen.s | . . . 4
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) | 
| 2 |  | spllen.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) | 
| 3 |  | spllen.t | . . . 4
⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) | 
| 4 |  | spllen.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ Word 𝐴) | 
| 5 |  | splval 14789 | . . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 6 | 1, 2, 3, 4, 5 | syl13anc 1374 | . . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 7 | 6 | fveq1d 6908 | . 2
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋)) | 
| 8 |  | pfxcl 14715 | . . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) | 
| 9 | 1, 8 | syl 17 | . . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) | 
| 10 |  | ccatcl 14612 | . . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) | 
| 11 | 9, 4, 10 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) | 
| 12 |  | swrdcl 14683 | . . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) | 
| 13 | 1, 12 | syl 17 | . . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) | 
| 14 | 2 | elfzelzd 13565 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ℤ) | 
| 15 | 14 | uzidd 12894 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℤ≥‘𝐹)) | 
| 16 |  | lencl 14571 | . . . . . . . 8
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) | 
| 17 | 4, 16 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘𝑅) ∈
ℕ0) | 
| 18 |  | uzaddcl 12946 | . . . . . . 7
⊢ ((𝐹 ∈
(ℤ≥‘𝐹) ∧ (♯‘𝑅) ∈ ℕ0) → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) | 
| 19 | 15, 17, 18 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) | 
| 20 |  | fzoss2 13727 | . . . . . 6
⊢ ((𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹) → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) | 
| 21 | 19, 20 | syl 17 | . . . . 5
⊢ (𝜑 → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) | 
| 22 |  | splfv1.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ (0..^𝐹)) | 
| 23 | 21, 22 | sseldd 3984 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(𝐹 + (♯‘𝑅)))) | 
| 24 |  | ccatlen 14613 | . . . . . . 7
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) | 
| 25 | 9, 4, 24 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) | 
| 26 |  | fzass4 13602 | . . . . . . . . . . 11
⊢ ((𝐹 ∈
(0...(♯‘𝑆))
∧ 𝑇 ∈ (𝐹...(♯‘𝑆))) ↔ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)))) | 
| 27 | 26 | biimpri 228 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → (𝐹 ∈ (0...(♯‘𝑆)) ∧ 𝑇 ∈ (𝐹...(♯‘𝑆)))) | 
| 28 | 27 | simpld 494 | . . . . . . . . 9
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → 𝐹 ∈ (0...(♯‘𝑆))) | 
| 29 | 2, 3, 28 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) | 
| 30 |  | pfxlen 14721 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 31 | 1, 29, 30 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 32 | 31 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) | 
| 33 | 25, 32 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = (𝐹 + (♯‘𝑅))) | 
| 34 | 33 | oveq2d 7447 | . . . 4
⊢ (𝜑 →
(0..^(♯‘((𝑆
prefix 𝐹) ++ 𝑅))) = (0..^(𝐹 + (♯‘𝑅)))) | 
| 35 | 23, 34 | eleqtrrd 2844 | . . 3
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) | 
| 36 |  | ccatval1 14615 | . . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) | 
| 37 | 11, 13, 35, 36 | syl3anc 1373 | . 2
⊢ (𝜑 → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) | 
| 38 | 31 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (0..^(♯‘(𝑆 prefix 𝐹))) = (0..^𝐹)) | 
| 39 | 22, 38 | eleqtrrd 2844 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) | 
| 40 |  | ccatval1 14615 | . . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) | 
| 41 | 9, 4, 39, 40 | syl3anc 1373 | . . 3
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) | 
| 42 |  | pfxfv 14720 | . . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆)) ∧ 𝑋 ∈ (0..^𝐹)) → ((𝑆 prefix 𝐹)‘𝑋) = (𝑆‘𝑋)) | 
| 43 | 1, 29, 22, 42 | syl3anc 1373 | . . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹)‘𝑋) = (𝑆‘𝑋)) | 
| 44 | 41, 43 | eqtrd 2777 | . 2
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = (𝑆‘𝑋)) | 
| 45 | 7, 37, 44 | 3eqtrd 2781 | 1
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = (𝑆‘𝑋)) |