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 14316 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1374 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
7 | 6 | fveq1d 6719 |
. 2
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋)) |
8 | | pfxcl 14242 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
10 | | ccatcl 14129 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 587 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 14210 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
14 | 2 | elfzelzd 13113 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ℤ) |
15 | 14 | uzidd 12454 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℤ≥‘𝐹)) |
16 | | lencl 14088 |
. . . . . . . 8
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) |
17 | 4, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑅) ∈
ℕ0) |
18 | | uzaddcl 12500 |
. . . . . . 7
⊢ ((𝐹 ∈
(ℤ≥‘𝐹) ∧ (♯‘𝑅) ∈ ℕ0) → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) |
19 | 15, 17, 18 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) |
20 | | fzoss2 13270 |
. . . . . 6
⊢ ((𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹) → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) |
22 | | splfv1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (0..^𝐹)) |
23 | 21, 22 | sseldd 3902 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(𝐹 + (♯‘𝑅)))) |
24 | | ccatlen 14130 |
. . . . . . 7
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
25 | 9, 4, 24 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
26 | | fzass4 13150 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈
(0...(♯‘𝑆))
∧ 𝑇 ∈ (𝐹...(♯‘𝑆))) ↔ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)))) |
27 | 26 | biimpri 231 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → (𝐹 ∈ (0...(♯‘𝑆)) ∧ 𝑇 ∈ (𝐹...(♯‘𝑆)))) |
28 | 27 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → 𝐹 ∈ (0...(♯‘𝑆))) |
29 | 2, 3, 28 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) |
30 | | pfxlen 14248 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
31 | 1, 29, 30 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
32 | 31 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) |
33 | 25, 32 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = (𝐹 + (♯‘𝑅))) |
34 | 33 | oveq2d 7229 |
. . . 4
⊢ (𝜑 →
(0..^(♯‘((𝑆
prefix 𝐹) ++ 𝑅))) = (0..^(𝐹 + (♯‘𝑅)))) |
35 | 23, 34 | eleqtrrd 2841 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) |
36 | | ccatval1 14133 |
. . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) |
37 | 11, 13, 35, 36 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) |
38 | 31 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → (0..^(♯‘(𝑆 prefix 𝐹))) = (0..^𝐹)) |
39 | 22, 38 | eleqtrrd 2841 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) |
40 | | ccatval1 14133 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) |
41 | 9, 4, 39, 40 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) |
42 | | pfxfv 14247 |
. . . 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 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = (𝑆‘𝑋)) |