Proof of Theorem splid
Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . 3
⊢ (𝑆 substr 〈𝑋, 𝑌〉) ∈ V |
2 | | splval 13502 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)) ∧ (𝑆 substr 〈𝑋, 𝑌〉) ∈ V)) → (𝑆 splice 〈𝑋, 𝑌, (𝑆 substr 〈𝑋, 𝑌〉)〉) = (((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉))) |
3 | 1, 2 | mp3anr3 1423 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (𝑆 splice 〈𝑋, 𝑌, (𝑆 substr 〈𝑋, 𝑌〉)〉) = (((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉))) |
4 | | simpl 473 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 𝑆 ∈ Word 𝐴) |
5 | | elfzuz 12338 |
. . . . . . 7
⊢ (𝑋 ∈ (0...𝑌) → 𝑋 ∈
(ℤ≥‘0)) |
6 | 5 | ad2antrl 764 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 𝑋 ∈
(ℤ≥‘0)) |
7 | | eluzfz1 12348 |
. . . . . 6
⊢ (𝑋 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑋)) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 0 ∈ (0...𝑋)) |
9 | | simprl 794 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 𝑋 ∈ (0...𝑌)) |
10 | | simprr 796 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 𝑌 ∈ (0...(#‘𝑆))) |
11 | | ccatswrd 13456 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (0 ∈ (0...𝑋) ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) = (𝑆 substr 〈0, 𝑌〉)) |
12 | 4, 8, 9, 10, 11 | syl13anc 1328 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) = (𝑆 substr 〈0, 𝑌〉)) |
13 | 12 | oveq1d 6665 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉)) = ((𝑆 substr 〈0, 𝑌〉) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉))) |
14 | | elfzuz 12338 |
. . . . . . 7
⊢ (𝑌 ∈ (0...(#‘𝑆)) → 𝑌 ∈
(ℤ≥‘0)) |
15 | 14 | ad2antll 765 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 𝑌 ∈
(ℤ≥‘0)) |
16 | | eluzfz1 12348 |
. . . . . 6
⊢ (𝑌 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑌)) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → 0 ∈ (0...𝑌)) |
18 | | elfzuz2 12346 |
. . . . . . 7
⊢ (𝑌 ∈ (0...(#‘𝑆)) → (#‘𝑆) ∈
(ℤ≥‘0)) |
19 | 18 | ad2antll 765 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (#‘𝑆) ∈
(ℤ≥‘0)) |
20 | | eluzfz2 12349 |
. . . . . 6
⊢
((#‘𝑆) ∈
(ℤ≥‘0) → (#‘𝑆) ∈ (0...(#‘𝑆))) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (#‘𝑆) ∈ (0...(#‘𝑆))) |
22 | | ccatswrd 13456 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ (0 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)) ∧ (#‘𝑆) ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈0, 𝑌〉) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉)) = (𝑆 substr 〈0, (#‘𝑆)〉)) |
23 | 4, 17, 10, 21, 22 | syl13anc 1328 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈0, 𝑌〉) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉)) = (𝑆 substr 〈0, (#‘𝑆)〉)) |
24 | | swrdid 13428 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, (#‘𝑆)〉) = 𝑆) |
25 | 24 | adantr 481 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (𝑆 substr 〈0, (#‘𝑆)〉) = 𝑆) |
26 | 23, 25 | eqtrd 2656 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈0, 𝑌〉) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉)) = 𝑆) |
27 | 13, 26 | eqtrd 2656 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (((𝑆 substr 〈0, 𝑋〉) ++ (𝑆 substr 〈𝑋, 𝑌〉)) ++ (𝑆 substr 〈𝑌, (#‘𝑆)〉)) = 𝑆) |
28 | 3, 27 | eqtrd 2656 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (𝑆 splice 〈𝑋, 𝑌, (𝑆 substr 〈𝑋, 𝑌〉)〉) = 𝑆) |