Step | Hyp | Ref
| Expression |
1 | | pfxcl 14121 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) ∈ Word 𝑉) |
2 | | revcl 14205 |
. . . . 5
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉) |
3 | | wrdfn 13962 |
. . . . 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 484 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿))))) |
6 | | revlen 14206 |
. . . . . . . 8
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
7 | 1, 6 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
8 | 7 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) |
9 | | pfxlen 14127 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐿)) = 𝐿) |
10 | 8, 9 | eqtrd 2773 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = 𝐿) |
11 | 10 | oveq2d 7180 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿)))) = (0..^𝐿)) |
12 | 11 | fneq2d 6426 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((reverse‘(𝑊 prefix
𝐿)) Fn
(0..^(♯‘(reverse‘(𝑊 prefix 𝐿)))) ↔ (reverse‘(𝑊 prefix 𝐿)) Fn (0..^𝐿))) |
13 | 5, 12 | mpbid 235 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) Fn (0..^𝐿)) |
14 | | revcl 14205 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (reverse‘𝑊) ∈ Word 𝑉) |
15 | | swrdcl 14089 |
. . . . 5
⊢
((reverse‘𝑊)
∈ Word 𝑉 →
((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)
∈ Word 𝑉) |
16 | | wrdfn 13962 |
. . . . 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 484 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)))) |
19 | | fznn0sub2 13098 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))) |
20 | | lencl 13967 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
21 | | nn0fz0 13089 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
22 | 20, 21 | sylib 221 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
23 | | revlen 14206 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
24 | 23 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 →
(0...(♯‘(reverse‘𝑊))) = (0...(♯‘𝑊))) |
25 | 22, 24 | eleqtrrd 2836 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
(0...(♯‘(reverse‘𝑊)))) |
26 | | swrdlen 14091 |
. . . . . . . 8
⊢
(((reverse‘𝑊)
∈ Word 𝑉 ∧
((♯‘𝑊) −
𝐿) ∈
(0...(♯‘𝑊))
∧ (♯‘𝑊)
∈ (0...(♯‘(reverse‘𝑊)))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
27 | 14, 19, 25, 26 | syl3an 1161 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
28 | 27 | 3anidm13 1421 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = ((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) |
29 | 20 | nn0cnd 12031 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈
ℂ) |
31 | | elfzelz 12991 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℤ) |
32 | 31 | zcnd 12162 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℂ) |
33 | 32 | adantl 485 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ ℂ) |
34 | 30, 33 | nncand 11073 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) = 𝐿) |
35 | 28, 34 | eqtrd 2773 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) = 𝐿) |
36 | 35 | oveq2d 7180 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉))) = (0..^𝐿)) |
37 | 36 | fneq2d 6426 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^(♯‘((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉))) ↔ ((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉) Fn
(0..^𝐿))) |
38 | 18, 37 | mpbid 235 |
. 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 7180 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^(♯‘(𝑊
prefix 𝐿))) = (0..^𝐿)) |
42 | 41 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (0..^(♯‘(𝑊 prefix 𝐿))) = (0..^𝐿)) |
43 | 40, 42 | eleqtrrd 2836 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) |
44 | | revfv 14207 |
. . . . . . 7
⊢ (((𝑊 prefix 𝐿) ∈ Word 𝑉 ∧ 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
45 | 1, 44 | sylan 583 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑥 ∈ (0..^(♯‘(𝑊 prefix 𝐿)))) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
46 | 39, 43, 45 | syl2anc 587 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = ((𝑊 prefix 𝐿)‘(((♯‘(𝑊 prefix 𝐿)) − 1) − 𝑥))) |
47 | 9 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((♯‘(𝑊 prefix
𝐿)) − 1) = (𝐿 − 1)) |
48 | 47 | oveq1d 7179 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(((♯‘(𝑊 prefix
𝐿)) − 1) −
𝑥) = ((𝐿 − 1) − 𝑥)) |
49 | 48 | fveq2d 6672 |
. . . . . 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 13122 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℤ) |
53 | 52 | zcnd 12162 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℂ) |
54 | 53 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ ℂ) |
55 | | 1cnd 10707 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 1 ∈ ℂ) |
56 | 51, 54, 55 | sub32d 11100 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 𝑥) − 1) = ((𝐿 − 1) − 𝑥)) |
57 | | ubmelm1fzo 13217 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝐿) → ((𝐿 − 𝑥) − 1) ∈ (0..^𝐿)) |
58 | 57 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 𝑥) − 1) ∈ (0..^𝐿)) |
59 | 56, 58 | eqeltrrd 2834 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝐿 − 1) − 𝑥) ∈ (0..^𝐿)) |
60 | | pfxfv 14126 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ ((𝐿 − 1) − 𝑥) ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥)) = (𝑊‘((𝐿 − 1) − 𝑥))) |
61 | 59, 60 | syld3an3 1410 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘((𝐿 − 1) − 𝑥)) = (𝑊‘((𝐿 − 1) − 𝑥))) |
62 | 46, 50, 61 | 3eqtrd 2777 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘(𝑊 prefix 𝐿))‘𝑥) = (𝑊‘((𝐿 − 1) − 𝑥))) |
63 | 34 | oveq2d 7180 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(0..^((♯‘𝑊)
− ((♯‘𝑊)
− 𝐿))) = (0..^𝐿)) |
64 | 63 | eleq2d 2818 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿))) ↔ 𝑥 ∈ (0..^𝐿))) |
65 | 64 | biimp3ar 1471 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) |
66 | | id 22 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉)) |
67 | 66 | 3anidm13 1421 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉)) |
68 | | swrdfv 14092 |
. . . . . . . . . 10
⊢
((((reverse‘𝑊)
∈ Word 𝑉 ∧
((♯‘𝑊) −
𝐿) ∈
(0...(♯‘𝑊))
∧ (♯‘𝑊)
∈ (0...(♯‘(reverse‘𝑊)))) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
69 | 14, 68 | syl3anl1 1413 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘(reverse‘𝑊)))) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
70 | 25, 69 | syl3anl3 1415 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
71 | 67, 70 | stoic3 1783 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
72 | 19, 71 | syl3an2 1165 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^((♯‘𝑊) − ((♯‘𝑊) − 𝐿)))) → (((reverse‘𝑊) substr
〈((♯‘𝑊)
− 𝐿),
(♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
73 | 65, 72 | syld3an3 1410 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥) = ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿)))) |
74 | | 0z 12066 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
75 | | elfzuz3 12988 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐿)) |
76 | 32 | addid2d 10912 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (0 + 𝐿) = 𝐿) |
77 | 76 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (ℤ≥‘(0 + 𝐿)) = (ℤ≥‘𝐿)) |
78 | 75, 77 | eleqtrrd 2836 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘(0 + 𝐿))) |
79 | | eluzsub 12349 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 𝐿
∈ ℤ ∧ (♯‘𝑊) ∈ (ℤ≥‘(0 +
𝐿))) →
((♯‘𝑊) −
𝐿) ∈
(ℤ≥‘0)) |
80 | 74, 31, 78, 79 | mp3an2i 1467 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(ℤ≥‘0)) |
81 | | fzoss1 13148 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
− 𝐿) ∈
(ℤ≥‘0) → (((♯‘𝑊) − 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (((♯‘𝑊)
− 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
83 | 82 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 𝐿)..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))) |
84 | 20 | nn0zd 12159 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ) |
85 | 84 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (♯‘𝑊) ∈ ℤ) |
86 | 31 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → 𝐿 ∈ ℤ) |
87 | 85, 86 | zsubcld 12166 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 𝐿) ∈ ℤ) |
88 | | fzo0addel 13175 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0..^𝐿) ∧ ((♯‘𝑊) − 𝐿) ∈ ℤ) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿)))) |
89 | 40, 87, 88 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿)))) |
90 | 30 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (♯‘𝑊) ∈ ℂ) |
91 | 51, 90 | pncan3d 11071 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝐿 + ((♯‘𝑊) − 𝐿)) = (♯‘𝑊)) |
92 | 91 | oveq2d 7180 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 𝐿)..^(𝐿 + ((♯‘𝑊) − 𝐿))) = (((♯‘𝑊) − 𝐿)..^(♯‘𝑊))) |
93 | 89, 92 | eleqtrd 2835 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (((♯‘𝑊) − 𝐿)..^(♯‘𝑊))) |
94 | 83, 93 | sseldd 3876 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (0..^(♯‘𝑊))) |
95 | | revfv 14207 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑥 + ((♯‘𝑊) − 𝐿)) ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿))) = (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))))) |
96 | 39, 94, 95 | syl2anc 587 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((reverse‘𝑊)‘(𝑥 + ((♯‘𝑊) − 𝐿))) = (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))))) |
97 | 90, 55 | subcld 11068 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 1) ∈
ℂ) |
98 | 87 | zcnd 12162 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − 𝐿) ∈ ℂ) |
99 | 97, 54, 98 | sub32d 11100 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) − 𝑥) − ((♯‘𝑊) − 𝐿)) = ((((♯‘𝑊) − 1) − ((♯‘𝑊) − 𝐿)) − 𝑥)) |
100 | 97, 54, 98 | subsub4d 11099 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) − 𝑥) − ((♯‘𝑊) − 𝐿)) = (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿)))) |
101 | 90, 55, 98 | sub32d 11100 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − ((♯‘𝑊) − 𝐿)) = (((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1)) |
102 | 101 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − 1) −
((♯‘𝑊) −
𝐿)) − 𝑥) = ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥)) |
103 | 99, 100, 102 | 3eqtr3d 2781 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))) = ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥)) |
104 | 34 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) = 𝐿) |
105 | 104 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) = (𝐿 − 1)) |
106 | 105 | oveq1d 7179 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → ((((♯‘𝑊) − ((♯‘𝑊) − 𝐿)) − 1) − 𝑥) = ((𝐿 − 1) − 𝑥)) |
107 | 103, 106 | eqtrd 2773 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿))) = ((𝐿 − 1) − 𝑥)) |
108 | 107 | fveq2d 6672 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (𝑊‘(((♯‘𝑊) − 1) − (𝑥 + ((♯‘𝑊) − 𝐿)))) = (𝑊‘((𝐿 − 1) − 𝑥))) |
109 | 73, 96, 108 | 3eqtrd 2777 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝑥 ∈ (0..^𝐿)) → (((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)‘𝑥) = (𝑊‘((𝐿 − 1) − 𝑥))) |
110 | 62, 109 | eqtr4d 2776 |
. . 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 6806 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr 〈((♯‘𝑊) − 𝐿), (♯‘𝑊)〉)) |