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 13953 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1365 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
7 | 6 | fveq2d 6549 |
. 2
⊢ (𝜑 → (♯‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) |
8 | | pfxcl 13879 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
10 | | ccatcl 13776 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 13847 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
14 | | ccatlen 13777 |
. . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) |
15 | 11, 13, 14 | syl2anc 584 |
. 2
⊢ (𝜑 → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) |
16 | | lencl 13733 |
. . . . . . 7
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) |
17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑅) ∈
ℕ0) |
18 | 17 | nn0cnd 11811 |
. . . . 5
⊢ (𝜑 → (♯‘𝑅) ∈
ℂ) |
19 | | elfzelz 12762 |
. . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℤ) |
20 | 2, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ℤ) |
21 | 20 | zcnd 11942 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) |
22 | 18, 21 | addcld 10513 |
. . . 4
⊢ (𝜑 → ((♯‘𝑅) + 𝐹) ∈ ℂ) |
23 | | elfzel2 12760 |
. . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ ℤ) |
24 | 3, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
ℤ) |
25 | 24 | zcnd 11942 |
. . . 4
⊢ (𝜑 → (♯‘𝑆) ∈
ℂ) |
26 | | elfzelz 12762 |
. . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ 𝑇 ∈
ℤ) |
27 | 3, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℤ) |
28 | 27 | zcnd 11942 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ℂ) |
29 | 22, 25, 28 | addsub12d 10874 |
. . 3
⊢ (𝜑 → (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇)) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) |
30 | | ccatlen 13777 |
. . . . . 6
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
31 | 9, 4, 30 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
32 | | elfzuz 12758 |
. . . . . . . . 9
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
(ℤ≥‘0)) |
33 | 2, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) |
34 | | elfzuz3 12759 |
. . . . . . . . . 10
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘𝑇)) |
35 | 3, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝑇)) |
36 | | elfzuz3 12759 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) |
37 | 2, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) |
38 | | uztrn 12114 |
. . . . . . . . 9
⊢
(((♯‘𝑆)
∈ (ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
39 | 35, 37, 38 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
40 | | elfzuzb 12756 |
. . . . . . . 8
⊢ (𝐹 ∈
(0...(♯‘𝑆))
↔ (𝐹 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝐹))) |
41 | 33, 39, 40 | sylanbrc 583 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) |
42 | | pfxlen 13885 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
43 | 1, 41, 42 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
44 | 43 | oveq1d 7038 |
. . . . 5
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) |
45 | 21, 18 | addcomd 10695 |
. . . . 5
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) = ((♯‘𝑅) + 𝐹)) |
46 | 31, 44, 45 | 3eqtrd 2837 |
. . . 4
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘𝑅) + 𝐹)) |
47 | | elfzuz2 12766 |
. . . . . . 7
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘0)) |
48 | 3, 47 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘0)) |
49 | | eluzfz2 12769 |
. . . . . 6
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (♯‘𝑆) ∈ (0...(♯‘𝑆))) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
(0...(♯‘𝑆))) |
51 | | swrdlen 13849 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ (♯‘𝑆) ∈
(0...(♯‘𝑆)))
→ (♯‘(𝑆
substr 〈𝑇,
(♯‘𝑆)〉)) =
((♯‘𝑆) −
𝑇)) |
52 | 1, 3, 50, 51 | syl3anc 1364 |
. . . 4
⊢ (𝜑 → (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((♯‘𝑆) − 𝑇)) |
53 | 46, 52 | oveq12d 7041 |
. . 3
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇))) |
54 | 18, 28, 21 | subsub3d 10881 |
. . . 4
⊢ (𝜑 → ((♯‘𝑅) − (𝑇 − 𝐹)) = (((♯‘𝑅) + 𝐹) − 𝑇)) |
55 | 54 | oveq2d 7039 |
. . 3
⊢ (𝜑 → ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹))) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) |
56 | 29, 53, 55 | 3eqtr4d 2843 |
. 2
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) |
57 | 7, 15, 56 | 3eqtrd 2837 |
1
⊢ (𝜑 → (♯‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) |