Proof of Theorem swrdpfx
Step | Hyp | Ref
| Expression |
1 | | elfznn0 13349 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 ∈
ℕ0) |
2 | 1 | anim2i 617 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
3 | 2 | adantr 481 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
4 | | pfxval 14386 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix 𝑁) = (𝑊 substr 〈0, 𝑁〉)) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 prefix 𝑁) = (𝑊 substr 〈0, 𝑁〉)) |
6 | 5 | oveq1d 7290 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 prefix 𝑁) substr 〈𝐾, 𝐿〉) = ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉)) |
7 | | simpl 483 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
8 | | simpr 485 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑁 ∈ (0...(♯‘𝑊))) |
9 | | 0elfz 13353 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
10 | 1, 9 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 0 ∈ (0...𝑁)) |
11 | 10 | adantl 482 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 0 ∈ (0...𝑁)) |
12 | 7, 8, 11 | 3jca 1127 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
13 | 12 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
14 | | elfzelz 13256 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 ∈
ℤ) |
15 | | zcn 12324 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
16 | 15 | subid1d 11321 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 − 0) = 𝑁) |
17 | 16 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 = (𝑁 − 0)) |
18 | 14, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 = (𝑁 − 0)) |
19 | 18 | adantl 482 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑁 = (𝑁 − 0)) |
20 | 19 | oveq2d 7291 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (0...𝑁) = (0...(𝑁 − 0))) |
21 | 20 | eleq2d 2824 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ∈ (0...(𝑁 − 0)))) |
22 | 19 | oveq2d 7291 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐾...𝑁) = (𝐾...(𝑁 − 0))) |
23 | 22 | eleq2d 2824 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐿 ∈ (𝐾...𝑁) ↔ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
24 | 21, 23 | anbi12d 631 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) ↔ (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0))))) |
25 | 24 | biimpa 477 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
26 | | swrdswrd 14418 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉))) |
27 | 13, 25, 26 | sylc 65 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉)) |
28 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
29 | 28 | zcnd 12427 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℂ) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℂ) |
31 | 30 | adantl 482 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐾 ∈ ℂ) |
32 | 31 | addid2d 11176 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐾) = 𝐾) |
33 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℤ) |
34 | 33 | zcnd 12427 |
. . . . . . . 8
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℂ) |
35 | 34 | adantl 482 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐿 ∈ ℂ) |
36 | 35 | adantl 482 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐿 ∈ ℂ) |
37 | 36 | addid2d 11176 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐿) = 𝐿) |
38 | 32, 37 | opeq12d 4812 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 〈(0 + 𝐾), (0 + 𝐿)〉 = 〈𝐾, 𝐿〉) |
39 | 38 | oveq2d 7291 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉) = (𝑊 substr 〈𝐾, 𝐿〉)) |
40 | 6, 27, 39 | 3eqtrd 2782 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 prefix 𝑁) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉)) |
41 | 40 | ex 413 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 prefix 𝑁) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) |