Step | Hyp | Ref
| Expression |
1 | | revcl 13361 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
2 | | revcl 13361 |
. . . 4
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘(reverse‘𝑊)) ∈ Word 𝐴) |
3 | | wrdf 13165 |
. . . 4
⊢
((reverse‘(reverse‘𝑊)) ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)):(0..^(#‘(reverse‘(reverse‘𝑊))))⟶𝐴) |
4 | | ffn 5958 |
. . . 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 13362 |
. . . . . . 7
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘(reverse‘𝑊))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘(reverse‘𝑊))) |
8 | | revlen 13362 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
9 | 7, 8 | eqtrd 2644 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 →
(#‘(reverse‘(reverse‘𝑊))) = (#‘𝑊)) |
10 | 9 | oveq2d 6565 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 →
(0..^(#‘(reverse‘(reverse‘𝑊)))) = (0..^(#‘𝑊))) |
11 | 10 | fneq2d 5896 |
. . 3
⊢ (𝑊 ∈ Word 𝐴 → ((reverse‘(reverse‘𝑊)) Fn
(0..^(#‘(reverse‘(reverse‘𝑊)))) ↔
(reverse‘(reverse‘𝑊)) Fn (0..^(#‘𝑊)))) |
12 | 5, 11 | mpbid 221 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) Fn (0..^(#‘𝑊))) |
13 | | wrdfn 13174 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(#‘𝑊))) |
14 | 1 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (reverse‘𝑊) ∈ Word 𝐴) |
15 | | simpr 476 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0..^(#‘𝑊))) |
16 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (#‘(reverse‘𝑊)) = (#‘𝑊)) |
17 | 16 | oveq2d 6565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
(0..^(#‘(reverse‘𝑊))) = (0..^(#‘𝑊))) |
18 | 15, 17 | eleqtrrd 2691 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0..^(#‘(reverse‘𝑊)))) |
19 | | revfv 13363 |
. . . 4
⊢
(((reverse‘𝑊)
∈ Word 𝐴 ∧ 𝑥 ∈
(0..^(#‘(reverse‘𝑊)))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥))) |
20 | 14, 18, 19 | syl2anc 691 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥))) |
21 | 16 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((#‘(reverse‘𝑊)) − 1) = ((#‘𝑊) − 1)) |
22 | 21 | oveq1d 6564 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘(reverse‘𝑊)) − 1) − 𝑥) = (((#‘𝑊) − 1) − 𝑥)) |
23 | 22 | fveq2d 6107 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥)) = ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥))) |
24 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈
ℕ0) |
25 | 24 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (#‘𝑊) ∈ ℤ) |
26 | | fzoval 12340 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐴 → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
28 | 27 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐴 → (𝑥 ∈ (0..^(#‘𝑊)) ↔ 𝑥 ∈ (0...((#‘𝑊) − 1)))) |
29 | 28 | biimpa 500 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → 𝑥 ∈ (0...((#‘𝑊) − 1))) |
30 | | fznn0sub2 12315 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...((#‘𝑊) − 1)) →
(((#‘𝑊) − 1)
− 𝑥) ∈
(0...((#‘𝑊) −
1))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0...((#‘𝑊) − 1))) |
32 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
33 | 31, 32 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) |
34 | | revfv 13363 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (((#‘𝑊) − 1) − 𝑥) ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)))) |
35 | 33, 34 | syldan 486 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)))) |
36 | | peano2zm 11297 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℤ → ((#‘𝑊)
− 1) ∈ ℤ) |
37 | 25, 36 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐴 → ((#‘𝑊) − 1) ∈
ℤ) |
38 | 37 | zcnd 11359 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → ((#‘𝑊) − 1) ∈
ℂ) |
39 | | elfzoelz 12339 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^(#‘𝑊)) → 𝑥 ∈ ℤ) |
40 | 39 | zcnd 11359 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^(#‘𝑊)) → 𝑥 ∈ ℂ) |
41 | | nncan 10189 |
. . . . . . 7
⊢
((((#‘𝑊)
− 1) ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((#‘𝑊) − 1) −
(((#‘𝑊) − 1)
− 𝑥)) = 𝑥) |
42 | 38, 40, 41 | syl2an 493 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥)) = 𝑥) |
43 | 42 | fveq2d 6107 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → (𝑊‘(((#‘𝑊) − 1) − (((#‘𝑊) − 1) − 𝑥))) = (𝑊‘𝑥)) |
44 | 35, 43 | eqtrd 2644 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘𝑊) − 1) − 𝑥)) = (𝑊‘𝑥)) |
45 | 23, 44 | eqtrd 2644 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘(((#‘(reverse‘𝑊)) − 1) − 𝑥)) = (𝑊‘𝑥)) |
46 | 20, 45 | eqtrd 2644 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(#‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = (𝑊‘𝑥)) |
47 | 12, 13, 46 | eqfnfvd 6222 |
1
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) |