Step | Hyp | Ref
| Expression |
1 | | revcl 13840 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) |
2 | | revcl 13840 |
. . . 4
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(reverse‘(reverse‘𝑊)) ∈ Word 𝐴) |
3 | | wrdf 13538 |
. . . 4
⊢
((reverse‘(reverse‘𝑊)) ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)):(0..^(♯‘(reverse‘(reverse‘𝑊))))⟶𝐴) |
4 | | ffn 6257 |
. . . 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 13841 |
. . . . . . 7
⊢
((reverse‘𝑊)
∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘(reverse‘𝑊))) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘(reverse‘𝑊))) |
8 | | revlen 13841 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
9 | 7, 8 | eqtrd 2834 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐴 →
(♯‘(reverse‘(reverse‘𝑊))) = (♯‘𝑊)) |
10 | 9 | oveq2d 6895 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 →
(0..^(♯‘(reverse‘(reverse‘𝑊)))) = (0..^(♯‘𝑊))) |
11 | 10 | fneq2d 6194 |
. . 3
⊢ (𝑊 ∈ Word 𝐴 → ((reverse‘(reverse‘𝑊)) Fn
(0..^(♯‘(reverse‘(reverse‘𝑊)))) ↔
(reverse‘(reverse‘𝑊)) Fn (0..^(♯‘𝑊)))) |
12 | 5, 11 | mpbid 224 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) Fn (0..^(♯‘𝑊))) |
13 | | wrdfn 13547 |
. 2
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(♯‘𝑊))) |
14 | 1 | adantr 473 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (reverse‘𝑊) ∈ Word 𝐴) |
15 | | simpr 478 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0..^(♯‘𝑊))) |
16 | 8 | adantr 473 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
(♯‘(reverse‘𝑊)) = (♯‘𝑊)) |
17 | 16 | oveq2d 6895 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
(0..^(♯‘(reverse‘𝑊))) = (0..^(♯‘𝑊))) |
18 | 15, 17 | eleqtrrd 2882 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈
(0..^(♯‘(reverse‘𝑊)))) |
19 | | revfv 13842 |
. . . 4
⊢
(((reverse‘𝑊)
∈ Word 𝐴 ∧ 𝑥 ∈
(0..^(♯‘(reverse‘𝑊)))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥))) |
20 | 14, 18, 19 | syl2anc 580 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥))) |
21 | 16 | oveq1d 6894 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((♯‘(reverse‘𝑊)) − 1) = ((♯‘𝑊) − 1)) |
22 | 21 | fvoveq1d 6901 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥)) = ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥))) |
23 | | lencl 13552 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈
ℕ0) |
24 | 23 | nn0zd 11769 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐴 → (♯‘𝑊) ∈ ℤ) |
25 | | fzoval 12725 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐴 → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
27 | 26 | eleq2d 2865 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐴 → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
28 | 27 | biimpa 469 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → 𝑥 ∈ (0...((♯‘𝑊) − 1))) |
29 | | fznn0sub2 12700 |
. . . . . . . 8
⊢ (𝑥 ∈
(0...((♯‘𝑊)
− 1)) → (((♯‘𝑊) − 1) − 𝑥) ∈ (0...((♯‘𝑊) − 1))) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0...((♯‘𝑊)
− 1))) |
31 | 26 | adantr 473 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
32 | 30, 31 | eleqtrrd 2882 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) − 𝑥) ∈
(0..^(♯‘𝑊))) |
33 | | revfv 13842 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (((♯‘𝑊) − 1) − 𝑥) ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥)))) |
34 | 32, 33 | syldan 586 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥)))) |
35 | | peano2zm 11709 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℤ → ((♯‘𝑊) − 1) ∈
ℤ) |
36 | 24, 35 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐴 → ((♯‘𝑊) − 1) ∈
ℤ) |
37 | 36 | zcnd 11772 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → ((♯‘𝑊) − 1) ∈
ℂ) |
38 | | elfzoelz 12724 |
. . . . . . . 8
⊢ (𝑥 ∈
(0..^(♯‘𝑊))
→ 𝑥 ∈
ℤ) |
39 | 38 | zcnd 11772 |
. . . . . . 7
⊢ (𝑥 ∈
(0..^(♯‘𝑊))
→ 𝑥 ∈
ℂ) |
40 | | nncan 10603 |
. . . . . . 7
⊢
((((♯‘𝑊)
− 1) ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(((♯‘𝑊) −
1) − (((♯‘𝑊) − 1) − 𝑥)) = 𝑥) |
41 | 37, 39, 40 | syl2an 590 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (((♯‘𝑊) − 1) −
(((♯‘𝑊) −
1) − 𝑥)) = 𝑥) |
42 | 41 | fveq2d 6416 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝑊‘(((♯‘𝑊) − 1) − (((♯‘𝑊) − 1) − 𝑥))) = (𝑊‘𝑥)) |
43 | 34, 42 | eqtrd 2834 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘𝑊) − 1) − 𝑥)) = (𝑊‘𝑥)) |
44 | 22, 43 | eqtrd 2834 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘(((♯‘(reverse‘𝑊)) − 1) − 𝑥)) = (𝑊‘𝑥)) |
45 | 20, 44 | eqtrd 2834 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) →
((reverse‘(reverse‘𝑊))‘𝑥) = (𝑊‘𝑥)) |
46 | 12, 13, 45 | eqfnfvd 6541 |
1
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) |