Step | Hyp | Ref
| Expression |
1 | | revcl 14358 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
2 | | revcl 14358 |
. . . 4
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘(reverse‘𝑊)) ∈ Word 𝐴) |
3 | | wrdf 14106 |
. . . 4
⊢
((reverse‘(reverse‘𝑊)) ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)):(0..^(♯‘(reverse‘(reverse‘𝑊))))⟶𝐴) |
4 | | ffn 6566 |
. . . 4
⊢
((reverse‘(reverse‘𝑊)):(0..^(♯‘(reverse‘(reverse‘𝑊))))⟶𝐴 → (reverse‘(reverse‘𝑊)) Fn
(0..^(♯‘(reverse‘(reverse‘𝑊))))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) Fn
(0..^(♯‘(reverse‘(reverse‘𝑊))))) |
6 | | revlen 14359 |
. . . . . . 7
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘(reverse‘𝑊))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘(reverse‘𝑊))) |
8 | | revlen 14359 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
9 | 7, 8 | eqtrd 2779 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘𝑊)) |
10 | 9 | oveq2d 7250 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 →
(0..^(♯‘(reverse‘(reverse‘𝑊)))) = (0..^(♯‘𝑊))) |
11 | 10 | fneq2d 6493 |
. . 3
⊢ (𝑊 ∈ Word 𝐴 → ((reverse‘(reverse‘𝑊)) Fn
(0..^(♯‘(reverse‘(reverse‘𝑊)))) ↔
(reverse‘(reverse‘𝑊)) Fn (0..^(♯‘𝑊)))) |
12 | 5, 11 | mpbid 235 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) Fn (0..^(♯‘𝑊))) |
13 | | wrdfn 14115 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
14 | | simpr 488 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0..^(♯‘𝑊))) |
15 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
(♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
16 | 15 | oveq2d 7250 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
(0..^(♯‘(reverse‘𝑊))) = (0..^(♯‘𝑊))) |
17 | 14, 16 | eleqtrrd 2843 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈
(0..^(♯‘(reverse‘𝑊)))) |
18 | | revfv 14360 |
. . . 4
⊢
(((reverse‘𝑊)
∈ Word 𝐴 ∧ 𝑥 ∈
(0..^(♯‘(reverse‘𝑊)))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥))) |
19 | 1, 17, 18 | syl2an2r 685 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥))) |
20 | 15 | oveq1d 7249 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((♯‘(reverse‘𝑊)) − 1) = ((♯‘𝑊) − 1)) |
21 | 20 | fvoveq1d 7256 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥)) = ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥))) |
22 | | lencl 14120 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈
ℕ0) |
23 | 22 | nn0zd 12309 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈ ℤ) |
24 | | fzoval 13273 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐴 → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
26 | 25 | eleq2d 2825 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐴 → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
27 | 26 | biimpa 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0...((♯‘𝑊) − 1))) |
28 | | fznn0sub2 13248 |
. . . . . . . 8
⊢ (𝑥 ∈
(0...((♯‘𝑊)
− 1)) → (((♯‘𝑊) − 1) − 𝑥) ∈ (0...((♯‘𝑊) − 1))) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0...((♯‘𝑊)
− 1))) |
30 | 25 | adantr 484 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
31 | 29, 30 | eleqtrrd 2843 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊))) |
32 | | revfv 14360 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (((♯‘𝑊) − 1) − 𝑥) ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥)))) |
33 | 31, 32 | syldan 594 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥)))) |
34 | | peano2zm 12249 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℤ → ((♯‘𝑊) − 1) ∈
ℤ) |
35 | 23, 34 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐴 → ((♯‘𝑊) − 1) ∈
ℤ) |
36 | 35 | zcnd 12312 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → ((♯‘𝑊) − 1) ∈
ℂ) |
37 | | elfzoelz 13272 |
. . . . . . . 8
⊢ (𝑥 ∈
(0..^(♯‘𝑊))
→ 𝑥 ∈
ℤ) |
38 | 37 | zcnd 12312 |
. . . . . . 7
⊢ (𝑥 ∈
(0..^(♯‘𝑊))
→ 𝑥 ∈
ℂ) |
39 | | nncan 11136 |
. . . . . . 7
⊢
((((♯‘𝑊)
− 1) ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(((♯‘𝑊) −
1) − (((♯‘𝑊) − 1) − 𝑥)) = 𝑥) |
40 | 36, 38, 39 | syl2an 599 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) −
(((♯‘𝑊) −
1) − 𝑥)) = 𝑥) |
41 | 40 | fveq2d 6742 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥))) = (𝑊‘𝑥)) |
42 | 33, 41 | eqtrd 2779 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘𝑥)) |
43 | 21, 42 | eqtrd 2779 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥)) = (𝑊‘𝑥)) |
44 | 19, 43 | eqtrd 2779 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = (𝑊‘𝑥)) |
45 | 12, 13, 44 | eqfnfvd 6876 |
1
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) |