Step | Hyp | Ref
| Expression |
1 | | revcl 13510 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
2 | | revcl 13510 |
. . . 4
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘(reverse‘𝑊)) ∈ Word 𝐴) |
3 | | wrdf 13310 |
. . . 4
⊢
((reverse‘(reverse‘𝑊)) ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)):(0..^(#‘(reverse‘(reverse‘𝑊))))⟶𝐴) |
4 | | ffn 6045 |
. . . 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 13511 |
. . . . . . 7
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘(reverse‘𝑊))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘(reverse‘𝑊))) |
8 | | revlen 13511 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
9 | 7, 8 | eqtrd 2656 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘𝑊)) |
10 | 9 | oveq2d 6666 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 →
(0..^(#‘(reverse‘(reverse‘𝑊)))) = (0..^(#‘𝑊))) |
11 | 10 | fneq2d 5982 |
. . 3
⊢ (𝑊 ∈ Word 𝐴 → ((reverse‘(reverse‘𝑊)) Fn
(0..^(#‘(reverse‘(reverse‘𝑊)))) ↔
(reverse‘(reverse‘𝑊)) Fn (0..^(#‘𝑊)))) |
12 | 5, 11 | mpbid 222 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) Fn (0..^(#‘𝑊))) |
13 | | wrdfn 13319 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(#‘𝑊))) |
14 | 1 | adantr 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (reverse‘𝑊) ∈ Word 𝐴) |
15 | | simpr 477 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0..^(#‘𝑊))) |
16 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
17 | 16 | oveq2d 6666 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
(0..^(#‘(reverse‘𝑊))) = (0..^(#‘𝑊))) |
18 | 15, 17 | eleqtrrd 2704 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0..^(#‘(reverse‘𝑊)))) |
19 | | revfv 13512 |
. . . 4
⊢
(((reverse‘𝑊)
∈ Word 𝐴 ∧ 𝑥 ∈
(0..^(#‘(reverse‘𝑊)))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥))) |
20 | 14, 18, 19 | syl2anc 693 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥))) |
21 | 16 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((#‘(reverse‘𝑊)) − 1) = ((#‘𝑊) − 1)) |
22 | 21 | oveq1d 6665 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘(reverse‘𝑊)) − 1) − 𝑥) = (((#‘𝑊) − 1) − 𝑥)) |
23 | 22 | fveq2d 6195 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥)) = ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥))) |
24 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈
ℕ0) |
25 | 24 | nn0zd 11480 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈ ℤ) |
26 | | fzoval 12471 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐴 → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
28 | 27 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐴 → (𝑥 ∈ (0..^(#‘𝑊)) ↔ 𝑥 ∈ (0...((#‘𝑊) − 1)))) |
29 | 28 | biimpa 501 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0...((#‘𝑊) − 1))) |
30 | | fznn0sub2 12446 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...((#‘𝑊) − 1)) →
(((#‘𝑊) − 1)
− 𝑥) ∈
(0...((#‘𝑊) −
1))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0...((#‘𝑊) − 1))) |
32 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
33 | 31, 32 | eleqtrrd 2704 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) |
34 | | revfv 13512 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)))) |
35 | 33, 34 | syldan 487 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)))) |
36 | | peano2zm 11420 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℤ → ((#‘𝑊)
− 1) ∈ ℤ) |
37 | 25, 36 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐴 → ((#‘𝑊) − 1) ∈
ℤ) |
38 | 37 | zcnd 11483 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → ((#‘𝑊) − 1) ∈
ℂ) |
39 | | elfzoelz 12470 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^(#‘𝑊)) → 𝑥 ∈ ℤ) |
40 | 39 | zcnd 11483 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^(#‘𝑊)) → 𝑥 ∈ ℂ) |
41 | | nncan 10310 |
. . . . . . 7
⊢
((((#‘𝑊)
− 1) ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((#‘𝑊) − 1) −
(((#‘𝑊) − 1)
− 𝑥)) = 𝑥) |
42 | 38, 40, 41 | syl2an 494 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)) = 𝑥) |
43 | 42 | fveq2d 6195 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥))) = (𝑊‘𝑥)) |
44 | 35, 43 | eqtrd 2656 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘𝑥)) |
45 | 23, 44 | eqtrd 2656 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥)) = (𝑊‘𝑥)) |
46 | 20, 45 | eqtrd 2656 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = (𝑊‘𝑥)) |
47 | 12, 13, 46 | eqfnfvd 6314 |
1
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) |