Step | Hyp | Ref
| Expression |
1 | | elfznn0 13541 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 ∈
ℕ0) |
2 | 1 | anim2i 618 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
3 | 2 | adantr 482 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈
ℕ0)) |
4 | | pfxval 14568 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix 𝑁) = (𝑊 substr ⟨0, 𝑁⟩)) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 prefix 𝑁) = (𝑊 substr ⟨0, 𝑁⟩)) |
6 | 5 | oveq1d 7377 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 prefix 𝑁) substr ⟨𝐾, 𝐿⟩) = ((𝑊 substr ⟨0, 𝑁⟩) substr ⟨𝐾, 𝐿⟩)) |
7 | | simpl 484 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
8 | | simpr 486 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑁 ∈ (0...(♯‘𝑊))) |
9 | | 0elfz 13545 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
10 | 1, 9 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 0 ∈ (0...𝑁)) |
11 | 10 | adantl 483 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 0 ∈ (0...𝑁)) |
12 | 7, 8, 11 | 3jca 1129 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
13 | 12 | adantr 482 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
14 | | elfzelz 13448 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 ∈
ℤ) |
15 | | zcn 12511 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
16 | 15 | subid1d 11508 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 − 0) = 𝑁) |
17 | 16 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 = (𝑁 − 0)) |
18 | 14, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(0...(♯‘𝑊))
→ 𝑁 = (𝑁 − 0)) |
19 | 18 | adantl 483 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑁 = (𝑁 − 0)) |
20 | 19 | oveq2d 7378 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (0...𝑁) = (0...(𝑁 − 0))) |
21 | 20 | eleq2d 2824 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ∈ (0...(𝑁 − 0)))) |
22 | 19 | oveq2d 7378 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐾...𝑁) = (𝐾...(𝑁 − 0))) |
23 | 22 | eleq2d 2824 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝐿 ∈ (𝐾...𝑁) ↔ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
24 | 21, 23 | anbi12d 632 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) ↔ (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0))))) |
25 | 24 | biimpa 478 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
26 | | swrdswrd 14600 |
. . . 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 13448 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
29 | 28 | zcnd 12615 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℂ) |
30 | 29 | adantr 482 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℂ) |
31 | 30 | adantl 483 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐾 ∈ ℂ) |
32 | 31 | addid2d 11363 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐾) = 𝐾) |
33 | | elfzelz 13448 |
. . . . . . . . 9
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℤ) |
34 | 33 | zcnd 12615 |
. . . . . . . 8
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℂ) |
35 | 34 | adantl 483 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐿 ∈ ℂ) |
36 | 35 | adantl 483 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐿 ∈ ℂ) |
37 | 36 | addid2d 11363 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐿) = 𝐿) |
38 | 32, 37 | opeq12d 4843 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ⟨(0 + 𝐾), (0 + 𝐿)⟩ = ⟨𝐾, 𝐿⟩) |
39 | 38 | oveq2d 7378 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 substr ⟨(0 + 𝐾), (0 + 𝐿)⟩) = (𝑊 substr ⟨𝐾, 𝐿⟩)) |
40 | 6, 27, 39 | 3eqtrd 2781 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 prefix 𝑁) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨𝐾, 𝐿⟩)) |
41 | 40 | ex 414 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 prefix 𝑁) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨𝐾, 𝐿⟩))) |