Proof of Theorem pfxpfx
Step | Hyp | Ref
| Expression |
1 | | elfznn0 12302 |
. . . . . 6
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈
ℕ0) |
2 | 1 | anim2i 591 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
3 | 2 | 3adant3 1074 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
4 | | pfxval 40246 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix 𝑁) = (𝑊 substr 〈0, 𝑁〉)) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 prefix 𝑁) = (𝑊 substr 〈0, 𝑁〉)) |
6 | 5 | oveq1d 6564 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 prefix 𝑁) prefix 𝐿) = ((𝑊 substr 〈0, 𝑁〉) prefix 𝐿)) |
7 | | simp1 1054 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → 𝑊 ∈ Word 𝑉) |
8 | | simp2 1055 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → 𝑁 ∈ (0...(#‘𝑊))) |
9 | | 0elfz 12305 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
10 | 1, 9 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 0 ∈ (0...𝑁)) |
11 | 10 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → 0 ∈ (0...𝑁)) |
12 | 7, 8, 11 | 3jca 1235 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
13 | 1 | nn0cnd 11230 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ ℂ) |
14 | 13 | subid1d 10260 |
. . . . . . . 8
⊢ (𝑁 ∈ (0...(#‘𝑊)) → (𝑁 − 0) = 𝑁) |
15 | 14 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 = (𝑁 − 0)) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → 𝑁 = (𝑁 − 0)) |
17 | 16 | oveq2d 6565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (0...𝑁) = (0...(𝑁 − 0))) |
18 | 17 | eleq2d 2673 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐿 ∈ (0...𝑁) ↔ 𝐿 ∈ (0...(𝑁 − 0)))) |
19 | 18 | biimp3a 1424 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → 𝐿 ∈ (0...(𝑁 − 0))) |
20 | | pfxswrd 40276 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 0)) → ((𝑊 substr 〈0, 𝑁〉) prefix 𝐿) = (𝑊 substr 〈0, (0 + 𝐿)〉))) |
21 | 12, 19, 20 | sylc 63 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) prefix 𝐿) = (𝑊 substr 〈0, (0 + 𝐿)〉)) |
22 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝐿 ∈ (0...𝑁) → 𝐿 ∈
ℕ0) |
23 | 22 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝐿 ∈ (0...𝑁) → 𝐿 ∈ ℂ) |
24 | 23 | addid2d 10116 |
. . . . . 6
⊢ (𝐿 ∈ (0...𝑁) → (0 + 𝐿) = 𝐿) |
25 | 24 | opeq2d 4347 |
. . . . 5
⊢ (𝐿 ∈ (0...𝑁) → 〈0, (0 + 𝐿)〉 = 〈0, 𝐿〉) |
26 | 25 | oveq2d 6565 |
. . . 4
⊢ (𝐿 ∈ (0...𝑁) → (𝑊 substr 〈0, (0 + 𝐿)〉) = (𝑊 substr 〈0, 𝐿〉)) |
27 | 26 | 3ad2ant3 1077 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 substr 〈0, (0 + 𝐿)〉) = (𝑊 substr 〈0, 𝐿〉)) |
28 | 22 | anim2i 591 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈
ℕ0)) |
29 | 28 | 3adant2 1073 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈
ℕ0)) |
30 | | pfxval 40246 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑊 prefix 𝐿) = (𝑊 substr 〈0, 𝐿〉)) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 prefix 𝐿) = (𝑊 substr 〈0, 𝐿〉)) |
32 | 27, 31 | eqtr4d 2647 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → (𝑊 substr 〈0, (0 + 𝐿)〉) = (𝑊 prefix 𝐿)) |
33 | 6, 21, 32 | 3eqtrd 2648 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 prefix 𝑁) prefix 𝐿) = (𝑊 prefix 𝐿)) |