Proof of Theorem spllen
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 13502 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1328 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
7 | 6 | fveq2d 6195 |
. 2
⊢ (𝜑 → (#‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = (#‘(((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉)))) |
8 | | swrdcl 13419 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
10 | | ccatcl 13359 |
. . . 4
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 13419 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
14 | | ccatlen 13360 |
. . 3
⊢ ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) → (#‘(((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) = ((#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) + (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉)))) |
15 | 11, 13, 14 | syl2anc 693 |
. 2
⊢ (𝜑 → (#‘(((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) = ((#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) + (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉)))) |
16 | | lencl 13324 |
. . . . . . 7
⊢ (𝑅 ∈ Word 𝐴 → (#‘𝑅) ∈
ℕ0) |
17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝑅) ∈
ℕ0) |
18 | 17 | nn0cnd 11353 |
. . . . 5
⊢ (𝜑 → (#‘𝑅) ∈ ℂ) |
19 | | elfzelz 12342 |
. . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℤ) |
20 | 2, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ℤ) |
21 | 20 | zcnd 11483 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) |
22 | 18, 21 | addcld 10059 |
. . . 4
⊢ (𝜑 → ((#‘𝑅) + 𝐹) ∈ ℂ) |
23 | | elfzel2 12340 |
. . . . . 6
⊢ (𝑇 ∈ (0...(#‘𝑆)) → (#‘𝑆) ∈
ℤ) |
24 | 3, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑆) ∈ ℤ) |
25 | 24 | zcnd 11483 |
. . . 4
⊢ (𝜑 → (#‘𝑆) ∈ ℂ) |
26 | | elfzelz 12342 |
. . . . . 6
⊢ (𝑇 ∈ (0...(#‘𝑆)) → 𝑇 ∈ ℤ) |
27 | 3, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℤ) |
28 | 27 | zcnd 11483 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ℂ) |
29 | 22, 25, 28 | addsub12d 10415 |
. . 3
⊢ (𝜑 → (((#‘𝑅) + 𝐹) + ((#‘𝑆) − 𝑇)) = ((#‘𝑆) + (((#‘𝑅) + 𝐹) − 𝑇))) |
30 | | ccatlen 13360 |
. . . . . 6
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
31 | 9, 4, 30 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
32 | | elfzuz 12338 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
(ℤ≥‘0)) |
33 | 2, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) |
34 | | eluzfz1 12348 |
. . . . . . . . 9
⊢ (𝐹 ∈
(ℤ≥‘0) → 0 ∈ (0...𝐹)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...𝐹)) |
36 | | elfzuz3 12339 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (0...(#‘𝑆)) → (#‘𝑆) ∈
(ℤ≥‘𝑇)) |
37 | 3, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑆) ∈ (ℤ≥‘𝑇)) |
38 | | elfzuz3 12339 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) |
39 | 2, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) |
40 | | uztrn 11704 |
. . . . . . . . . 10
⊢
(((#‘𝑆) ∈
(ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (#‘𝑆) ∈
(ℤ≥‘𝐹)) |
41 | 37, 39, 40 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑆) ∈ (ℤ≥‘𝐹)) |
42 | | elfzuzb 12336 |
. . . . . . . . 9
⊢ (𝐹 ∈ (0...(#‘𝑆)) ↔ (𝐹 ∈ (ℤ≥‘0)
∧ (#‘𝑆) ∈
(ℤ≥‘𝐹))) |
43 | 33, 41, 42 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (0...(#‘𝑆))) |
44 | | swrdlen 13423 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 0 ∈ (0...𝐹) ∧ 𝐹 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
45 | 1, 35, 43, 44 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
46 | 21 | subid1d 10381 |
. . . . . . 7
⊢ (𝜑 → (𝐹 − 0) = 𝐹) |
47 | 45, 46 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = 𝐹) |
48 | 47 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅)) = (𝐹 + (#‘𝑅))) |
49 | 21, 18 | addcomd 10238 |
. . . . 5
⊢ (𝜑 → (𝐹 + (#‘𝑅)) = ((#‘𝑅) + 𝐹)) |
50 | 31, 48, 49 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘𝑅) + 𝐹)) |
51 | | elfzuz2 12346 |
. . . . . . 7
⊢ (𝑇 ∈ (0...(#‘𝑆)) → (#‘𝑆) ∈
(ℤ≥‘0)) |
52 | 3, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈
(ℤ≥‘0)) |
53 | | eluzfz2 12349 |
. . . . . 6
⊢
((#‘𝑆) ∈
(ℤ≥‘0) → (#‘𝑆) ∈ (0...(#‘𝑆))) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑆) ∈ (0...(#‘𝑆))) |
55 | | swrdlen 13423 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ (0...(#‘𝑆)) ∧ (#‘𝑆) ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉)) = ((#‘𝑆) − 𝑇)) |
56 | 1, 3, 54, 55 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉)) = ((#‘𝑆) − 𝑇)) |
57 | 50, 56 | oveq12d 6668 |
. . 3
⊢ (𝜑 → ((#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) + (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉))) = (((#‘𝑅) + 𝐹) + ((#‘𝑆) − 𝑇))) |
58 | 18, 28, 21 | subsub3d 10422 |
. . . 4
⊢ (𝜑 → ((#‘𝑅) − (𝑇 − 𝐹)) = (((#‘𝑅) + 𝐹) − 𝑇)) |
59 | 58 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((#‘𝑆) + ((#‘𝑅) − (𝑇 − 𝐹))) = ((#‘𝑆) + (((#‘𝑅) + 𝐹) − 𝑇))) |
60 | 29, 57, 59 | 3eqtr4d 2666 |
. 2
⊢ (𝜑 → ((#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) + (#‘(𝑆 substr 〈𝑇, (#‘𝑆)〉))) = ((#‘𝑆) + ((#‘𝑅) − (𝑇 − 𝐹)))) |
61 | 7, 15, 60 | 3eqtrd 2660 |
1
⊢ (𝜑 → (#‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = ((#‘𝑆) + ((#‘𝑅) − (𝑇 − 𝐹)))) |