Step |
Hyp |
Ref |
Expression |
1 |
|
revval |
|- ( W e. Word A -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ) |
2 |
1
|
fveq1d |
|- ( W e. Word A -> ( ( reverse ` W ) ` X ) = ( ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ` X ) ) |
3 |
|
oveq2 |
|- ( x = X -> ( ( ( # ` W ) - 1 ) - x ) = ( ( ( # ` W ) - 1 ) - X ) ) |
4 |
3
|
fveq2d |
|- ( x = X -> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) = ( W ` ( ( ( # ` W ) - 1 ) - X ) ) ) |
5 |
|
eqid |
|- ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) |
6 |
|
fvex |
|- ( W ` ( ( ( # ` W ) - 1 ) - X ) ) e. _V |
7 |
4 5 6
|
fvmpt |
|- ( X e. ( 0 ..^ ( # ` W ) ) -> ( ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ` X ) = ( W ` ( ( ( # ` W ) - 1 ) - X ) ) ) |
8 |
2 7
|
sylan9eq |
|- ( ( W e. Word A /\ X e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` X ) = ( W ` ( ( ( # ` W ) - 1 ) - X ) ) ) |