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 13353 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1320 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
7 | 6 | fveq1d 6105 |
. 2
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘𝑋)) |
8 | | swrdcl 13271 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
10 | | ccatcl 13212 |
. . . 4
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 13271 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
14 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℤ) |
15 | | uzid 11578 |
. . . . . . . 8
⊢ (𝐹 ∈ ℤ → 𝐹 ∈
(ℤ≥‘𝐹)) |
16 | 2, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℤ≥‘𝐹)) |
17 | | wrdfin 13178 |
. . . . . . . 8
⊢ (𝑅 ∈ Word 𝐴 → 𝑅 ∈ Fin) |
18 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝑅 ∈ Fin →
(#‘𝑅) ∈
ℕ0) |
19 | 4, 17, 18 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑅) ∈
ℕ0) |
20 | | uzaddcl 11620 |
. . . . . . 7
⊢ ((𝐹 ∈
(ℤ≥‘𝐹) ∧ (#‘𝑅) ∈ ℕ0) → (𝐹 + (#‘𝑅)) ∈
(ℤ≥‘𝐹)) |
21 | 16, 19, 20 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐹 + (#‘𝑅)) ∈
(ℤ≥‘𝐹)) |
22 | | fzoss2 12365 |
. . . . . 6
⊢ ((𝐹 + (#‘𝑅)) ∈
(ℤ≥‘𝐹) → (0..^𝐹) ⊆ (0..^(𝐹 + (#‘𝑅)))) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^𝐹) ⊆ (0..^(𝐹 + (#‘𝑅)))) |
24 | | splfv1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (0..^𝐹)) |
25 | 23, 24 | sseldd 3569 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(𝐹 + (#‘𝑅)))) |
26 | | ccatlen 13213 |
. . . . . . 7
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
27 | 9, 4, 26 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
28 | | elfzuz 12209 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
(ℤ≥‘0)) |
29 | | eluzfz1 12219 |
. . . . . . . . . 10
⊢ (𝐹 ∈
(ℤ≥‘0) → 0 ∈ (0...𝐹)) |
30 | 2, 28, 29 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝐹)) |
31 | | fzass4 12250 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (0...(#‘𝑆)) ∧ 𝑇 ∈ (𝐹...(#‘𝑆))) ↔ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆)))) |
32 | 31 | bicomi 213 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆))) ↔ (𝐹 ∈ (0...(#‘𝑆)) ∧ 𝑇 ∈ (𝐹...(#‘𝑆)))) |
33 | 32 | simplbi 475 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆))) → 𝐹 ∈ (0...(#‘𝑆))) |
34 | 2, 3, 33 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (0...(#‘𝑆))) |
35 | | swrdlen 13275 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 0 ∈ (0...𝐹) ∧ 𝐹 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
36 | 1, 30, 34, 35 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
37 | 2, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) |
38 | 37 | zcnd 11359 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ℂ) |
39 | 38 | subid1d 10260 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 − 0) = 𝐹) |
40 | 36, 39 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = 𝐹) |
41 | 40 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅)) = (𝐹 + (#‘𝑅))) |
42 | 27, 41 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = (𝐹 + (#‘𝑅))) |
43 | 42 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅))) = (0..^(𝐹 + (#‘𝑅)))) |
44 | 25, 43 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) |
45 | | ccatval1 13214 |
. . 3
⊢ ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) → ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘𝑋) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘𝑋)) |
46 | 11, 13, 44, 45 | syl3anc 1318 |
. 2
⊢ (𝜑 → ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘𝑋) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘𝑋)) |
47 | 40 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0..^(#‘(𝑆 substr 〈0, 𝐹〉))) = (0..^𝐹)) |
48 | 24, 47 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(#‘(𝑆 substr 〈0, 𝐹〉)))) |
49 | | ccatval1 13214 |
. . . 4
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(#‘(𝑆 substr 〈0, 𝐹〉)))) → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘𝑋) = ((𝑆 substr 〈0, 𝐹〉)‘𝑋)) |
50 | 9, 4, 48, 49 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘𝑋) = ((𝑆 substr 〈0, 𝐹〉)‘𝑋)) |
51 | 39 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0..^(𝐹 − 0)) = (0..^𝐹)) |
52 | 24, 51 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (0..^(𝐹 − 0))) |
53 | | swrdfv 13276 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 0 ∈ (0...𝐹) ∧ 𝐹 ∈ (0...(#‘𝑆))) ∧ 𝑋 ∈ (0..^(𝐹 − 0))) → ((𝑆 substr 〈0, 𝐹〉)‘𝑋) = (𝑆‘(𝑋 + 0))) |
54 | 1, 30, 34, 52, 53 | syl31anc 1321 |
. . 3
⊢ (𝜑 → ((𝑆 substr 〈0, 𝐹〉)‘𝑋) = (𝑆‘(𝑋 + 0))) |
55 | | elfzoelz 12339 |
. . . . . . 7
⊢ (𝑋 ∈ (0..^𝐹) → 𝑋 ∈ ℤ) |
56 | 55 | zcnd 11359 |
. . . . . 6
⊢ (𝑋 ∈ (0..^𝐹) → 𝑋 ∈ ℂ) |
57 | 24, 56 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
58 | 57 | addid1d 10115 |
. . . 4
⊢ (𝜑 → (𝑋 + 0) = 𝑋) |
59 | 58 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (𝑆‘(𝑋 + 0)) = (𝑆‘𝑋)) |
60 | 50, 54, 59 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘𝑋) = (𝑆‘𝑋)) |
61 | 7, 46, 60 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = (𝑆‘𝑋)) |