Metamath Proof Explorer


Theorem revfv

Description: Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revfv
|- ( ( W e. Word A /\ X e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` X ) = ( W ` ( ( ( # ` W ) - 1 ) - X ) ) )

Proof

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 ) ) )