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