Step |
Hyp |
Ref |
Expression |
1 |
|
revcl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) ∈ Word 𝐴 ) |
2 |
|
revcl |
⊢ ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) ∈ Word 𝐴 ) |
3 |
|
wrdf |
⊢ ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ⟶ 𝐴 ) |
4 |
|
ffn |
⊢ ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ⟶ 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ) |
5 |
1 2 3 4
|
4syl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ) |
6 |
|
revlen |
⊢ ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) |
7 |
1 6
|
syl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) |
8 |
|
revlen |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) ) |
9 |
7 8
|
eqtrd |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) ) |
10 |
9
|
oveq2d |
⊢ ( 𝑊 ∈ Word 𝐴 → ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
11 |
10
|
fneq2d |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ↔ ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) |
12 |
5 11
|
mpbid |
⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
13 |
|
wrdfn |
⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
14 |
|
simpr |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
15 |
8
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) ) |
16 |
15
|
oveq2d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
17 |
14 16
|
eleqtrrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ) |
18 |
|
revfv |
⊢ ( ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) |
19 |
1 17 18
|
syl2an2r |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) |
20 |
15
|
oveq1d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) |
21 |
20
|
fvoveq1d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) |
22 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
23 |
22
|
nn0zd |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℤ ) |
24 |
|
fzoval |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
25 |
23 24
|
syl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
26 |
25
|
eleq2d |
⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ) |
27 |
26
|
biimpa |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
28 |
|
fznn0sub2 |
⊢ ( 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
29 |
27 28
|
syl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
30 |
25
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
31 |
29 30
|
eleqtrrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
32 |
|
revfv |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ) |
33 |
31 32
|
syldan |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ) |
34 |
|
peano2zm |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ) |
35 |
23 34
|
syl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ) |
36 |
35
|
zcnd |
⊢ ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ ) |
37 |
|
elfzoelz |
⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑥 ∈ ℤ ) |
38 |
37
|
zcnd |
⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑥 ∈ ℂ ) |
39 |
|
nncan |
⊢ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = 𝑥 ) |
40 |
36 38 39
|
syl2an |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = 𝑥 ) |
41 |
40
|
fveq2d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) = ( 𝑊 ‘ 𝑥 ) ) |
42 |
33 41
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ 𝑥 ) ) |
43 |
21 42
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ 𝑥 ) ) |
44 |
19 43
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) ) |
45 |
12 13 44
|
eqfnfvd |
⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) = 𝑊 ) |