| Step | Hyp | Ref
| Expression |
| 1 | | pfxcl 14715 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) ∈ Word 𝑉) |
| 2 | | revcl 14799 |
. . . . 5
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉) |
| 3 | | wrdfn 14566 |
. . . . 5
⊢
((reverse‘(𝑊
prefix 𝐿)) ∈ Word
𝑉 →
(reverse‘(𝑊 prefix
𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿))))) |
| 4 | 1, 2, 3 | 3syl 18 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (reverse‘(𝑊 prefix 𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿))))) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿))))) |
| 6 | | revlen 14800 |
. . . . . . . 8
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
| 7 | 1, 6 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
| 9 | | pfxlen 14721 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐿)) = 𝐿) |
| 10 | 8, 9 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = 𝐿) |
| 11 | 10 | oveq2d 7447 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿)))) = (0..^𝐿)) |
| 12 | 11 | fneq2d 6662 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((reverse‘(𝑊 prefix
𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿)))) ↔ (reverse‘(𝑊 prefix 𝐿)) Fn (0..^𝐿))) |
| 13 | 5, 12 | mpbid 232 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) Fn (0..^𝐿)) |
| 14 | | revcl 14799 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (reverse‘𝑊) ∈ Word 𝑉) |
| 15 | | swrdcl 14683 |
. . . . 5
⊢
((reverse‘𝑊)
∈ Word 𝑉 →
((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)
∈ Word 𝑉) |
| 16 | | wrdfn 14566 |
. . . . 5
⊢
(((reverse‘𝑊)
substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉) ∈ Word 𝑉 → ((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)))) |
| 17 | 14, 15, 16 | 3syl 18 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)))) |
| 18 | 17 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)))) |
| 19 | | fznn0sub2 13675 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))) |
| 20 | | lencl 14571 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
| 21 | | nn0fz0 13665 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 23 | | revlen 14800 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
| 24 | 23 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 →
(0...(♯‘(reverse‘𝑊))) = (0...(♯‘𝑊))) |
| 25 | 22, 24 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
(0...(♯‘(reverse‘𝑊)))) |
| 26 | | swrdlen 14685 |
. . . . . . . 8
⊢
(((reverse‘𝑊)
∈ Word 𝑉 ∧
((♯‘𝑊) −
𝐿) ∈
(0...(♯‘𝑊))
∧ (♯‘𝑊)
∈ (0...(♯‘(reverse‘𝑊)))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
| 27 | 14, 19, 25, 26 | syl3an 1161 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
| 28 | 27 | 3anidm13 1422 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
| 29 | 20 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈
ℂ) |
| 31 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℤ) |
| 32 | 31 | zcnd 12723 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℂ) |
| 33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ ℂ) |
| 34 | 30, 33 | nncand 11625 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) = 𝐿) |
| 35 | 28, 34 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = 𝐿) |
| 36 | 35 | oveq2d 7447 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉))) = (0..^𝐿)) |
| 37 | 36 | fneq2d 6662 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉))) ↔ ((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^𝐿))) |
| 38 | 18, 37 | mpbid 232 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^𝐿)) |
| 39 | | simp1 1137 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑊 ∈ Word 𝑉) |
| 40 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ (0..^𝐿)) |
| 41 | 9 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘(𝑊
prefix 𝐿))) = (0..^𝐿)) |
| 42 | 41 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (0..^(♯‘(𝑊 prefix 𝐿))) = (0..^𝐿)) |
| 43 | 40, 42 | eleqtrrd 2844 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) |
| 44 | | revfv 14801 |
. . . . . . 7
⊢ (((𝑊 prefix 𝐿) ∈ Word 𝑉 ∧ 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
| 45 | 1, 44 | sylan 580 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
| 46 | 39, 43, 45 | syl2anc 584 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
| 47 | 9 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((♯‘(𝑊 prefix
𝐿)) − 1) = (𝐿 − 1)) |
| 48 | 47 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(((♯‘(𝑊 prefix
𝐿)) − 1) −
𝑥) = ((𝐿 − 1) − 𝑥)) |
| 49 | 48 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥)) = ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥))) |
| 50 | 49 | 3adant3 1133 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥)) = ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥))) |
| 51 | 32 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝐿 ∈ ℂ) |
| 52 | | elfzoelz 13699 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℤ) |
| 53 | 52 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℂ) |
| 54 | 53 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ ℂ) |
| 55 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 1 ∈ ℂ) |
| 56 | 51, 54, 55 | sub32d 11652 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 𝑥) − 1) = ((𝐿 − 1) − 𝑥)) |
| 57 | | ubmelm1fzo 13802 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝐿) → ((𝐿 − 𝑥) − 1) ∈ (0..^𝐿)) |
| 58 | 57 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 𝑥) − 1) ∈ (0..^𝐿)) |
| 59 | 56, 58 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 1) − 𝑥) ∈ (0..^𝐿)) |
| 60 | | pfxfv 14720 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ ((𝐿 − 1) − 𝑥) ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥)) = (𝑊‘((𝐿 − 1) − 𝑥))) |
| 61 | 59, 60 | syld3an3 1411 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥)) = (𝑊‘((𝐿 − 1) − 𝑥))) |
| 62 | 46, 50, 61 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = (𝑊‘((𝐿 − 1) − 𝑥))) |
| 63 | 34 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^((♯‘𝑊)
− ((♯‘𝑊)
− 𝐿))) = (0..^𝐿)) |
| 64 | 63 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) ↔ 𝑥 ∈ (0..^𝐿))) |
| 65 | 64 | biimp3ar 1472 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) |
| 66 | | id 22 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉)) |
| 67 | 66 | 3anidm13 1422 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉)) |
| 68 | | swrdfv 14686 |
. . . . . . . . . 10
⊢
((((reverse‘𝑊)
∈ Word 𝑉 ∧
((♯‘𝑊) −
𝐿) ∈
(0...(♯‘𝑊))
∧ (♯‘𝑊)
∈ (0...(♯‘(reverse‘𝑊)))) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 69 | 14, 68 | syl3anl1 1414 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘(reverse‘𝑊)))) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 70 | 25, 69 | syl3anl3 1416 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 71 | 67, 70 | stoic3 1776 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 72 | 19, 71 | syl3an2 1165 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 73 | 65, 72 | syld3an3 1411 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 74 | | 0z 12624 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
| 75 | | elfzuz3 13561 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐿)) |
| 76 | 32 | addlidd 11462 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (0 + 𝐿) = 𝐿) |
| 77 | 76 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (ℤ≥‘(0 + 𝐿)) = (ℤ≥‘𝐿)) |
| 78 | 75, 77 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘(0 + 𝐿))) |
| 79 | | eluzsub 12908 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ (♯‘𝑊) ∈ (ℤ≥‘(0 +
𝐿))) →
((♯‘𝑊) −
𝐿) ∈
(ℤ≥‘0)) |
| 80 | 74, 31, 78, 79 | mp3an2i 1468 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(ℤ≥‘0)) |
| 81 | | fzoss1 13726 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
− 𝐿) ∈
(ℤ≥‘0) → (((♯‘𝑊) − 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
| 82 | 80, 81 | syl 17 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (((♯‘𝑊)
− 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
| 83 | 82 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
| 84 | 20 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ) |
| 85 | 84 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (♯‘𝑊) ∈ ℤ) |
| 86 | 31 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝐿 ∈ ℤ) |
| 87 | 85, 86 | zsubcld 12727 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 𝐿) ∈ ℤ) |
| 88 | | fzo0addel 13757 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0..^𝐿) ∧ ((♯‘𝑊) − 𝐿) ∈ ℤ) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿)))) |
| 89 | 40, 87, 88 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿)))) |
| 90 | 30 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (♯‘𝑊) ∈ ℂ) |
| 91 | 51, 90 | pncan3d 11623 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝐿 + ((♯‘𝑊) − 𝐿)) = (♯‘𝑊)) |
| 92 | 91 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿))) = (((♯‘𝑊) − 𝐿)..^(♯‘𝑊))) |
| 93 | 89, 92 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(♯‘𝑊))) |
| 94 | 83, 93 | sseldd 3984 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (0..^(♯‘𝑊))) |
| 95 | | revfv 14801 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿))) = (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))))) |
| 96 | 39, 94, 95 | syl2anc 584 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿))) = (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))))) |
| 97 | 90, 55 | subcld 11620 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 1) ∈
ℂ) |
| 98 | 87 | zcnd 12723 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 𝐿) ∈ ℂ) |
| 99 | 97, 54, 98 | sub32d 11652 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) − 𝑥) − ((♯‘𝑊) − 𝐿)) = ((((♯‘𝑊) − 1) − ((♯‘𝑊) − 𝐿)) − 𝑥)) |
| 100 | 97, 54, 98 | subsub4d 11651 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) − 𝑥) − ((♯‘𝑊) − 𝐿)) = (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿)))) |
| 101 | 90, 55, 98 | sub32d 11652 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − ((♯‘𝑊) − 𝐿)) = (((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1)) |
| 102 | 101 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) −
((♯‘𝑊) −
𝐿)) − 𝑥) = ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥)) |
| 103 | 99, 100, 102 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))) = ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥)) |
| 104 | 34 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) = 𝐿) |
| 105 | 104 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) = (𝐿 − 1)) |
| 106 | 105 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥) = ((𝐿 − 1) − 𝑥)) |
| 107 | 103, 106 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))) = ((𝐿 − 1) − 𝑥)) |
| 108 | 107 | fveq2d 6910 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿)))) = (𝑊‘((𝐿 − 1) − 𝑥))) |
| 109 | 73, 96, 108 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥) = (𝑊‘((𝐿 − 1) − 𝑥))) |
| 110 | 62, 109 | eqtr4d 2780 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥)) |
| 111 | 110 | 3expa 1119 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥)) |
| 112 | 13, 38, 111 | eqfnfvd 7054 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) |