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 14646 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1373 |
. . 3
⊢ (𝜑 → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |
7 | 6 | fveq1d 6849 |
. 2
⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘𝑋) = ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))‘𝑋)) |
8 | | pfxcl 14572 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
10 | | ccatcl 14469 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 585 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 14540 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴) |
14 | 2 | elfzelzd 13449 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ℤ) |
15 | 14 | uzidd 12786 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℤ≥‘𝐹)) |
16 | | lencl 14428 |
. . . . . . . 8
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) |
17 | 4, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑅) ∈
ℕ0) |
18 | | uzaddcl 12836 |
. . . . . . 7
⊢ ((𝐹 ∈
(ℤ≥‘𝐹) ∧ (♯‘𝑅) ∈ ℕ0) → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) |
19 | 15, 17, 18 | syl2anc 585 |
. . . . . 6
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹)) |
20 | | fzoss2 13607 |
. . . . . 6
⊢ ((𝐹 + (♯‘𝑅)) ∈
(ℤ≥‘𝐹) → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^𝐹) ⊆ (0..^(𝐹 + (♯‘𝑅)))) |
22 | | splfv1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (0..^𝐹)) |
23 | 21, 22 | sseldd 3950 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(𝐹 + (♯‘𝑅)))) |
24 | | ccatlen 14470 |
. . . . . . 7
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
25 | 9, 4, 24 | syl2anc 585 |
. . . . . 6
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
26 | | fzass4 13486 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈
(0...(♯‘𝑆))
∧ 𝑇 ∈ (𝐹...(♯‘𝑆))) ↔ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)))) |
27 | 26 | biimpri 227 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → (𝐹 ∈ (0...(♯‘𝑆)) ∧ 𝑇 ∈ (𝐹...(♯‘𝑆)))) |
28 | 27 | simpld 496 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → 𝐹 ∈ (0...(♯‘𝑆))) |
29 | 2, 3, 28 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) |
30 | | pfxlen 14578 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
31 | 1, 29, 30 | syl2anc 585 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
32 | 31 | oveq1d 7377 |
. . . . . 6
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) |
33 | 25, 32 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = (𝐹 + (♯‘𝑅))) |
34 | 33 | oveq2d 7378 |
. . . 4
⊢ (𝜑 →
(0..^(♯‘((𝑆
prefix 𝐹) ++ 𝑅))) = (0..^(𝐹 + (♯‘𝑅)))) |
35 | 23, 34 | eleqtrrd 2841 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) |
36 | | ccatval1 14472 |
. . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) |
37 | 11, 13, 35, 36 | syl3anc 1372 |
. 2
⊢ (𝜑 → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))‘𝑋) = (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋)) |
38 | 31 | oveq2d 7378 |
. . . . 5
⊢ (𝜑 → (0..^(♯‘(𝑆 prefix 𝐹))) = (0..^𝐹)) |
39 | 22, 38 | eleqtrrd 2841 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) |
40 | | ccatval1 14472 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘(𝑆 prefix 𝐹)))) → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) |
41 | 9, 4, 39, 40 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = ((𝑆 prefix 𝐹)‘𝑋)) |
42 | | pfxfv 14577 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆)) ∧ 𝑋 ∈ (0..^𝐹)) → ((𝑆 prefix 𝐹)‘𝑋) = (𝑆‘𝑋)) |
43 | 1, 29, 22, 42 | syl3anc 1372 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹)‘𝑋) = (𝑆‘𝑋)) |
44 | 41, 43 | eqtrd 2777 |
. 2
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘𝑋) = (𝑆‘𝑋)) |
45 | 7, 37, 44 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘𝑋) = (𝑆‘𝑋)) |