Metamath Proof Explorer

Theorem revval

Description: Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revval 
|- ( W e. V -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( W e. V -> W e. _V )
2 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
3 2 oveq2d 
 |-  ( w = W -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` W ) ) )
4 id 
 |-  ( w = W -> w = W )
5 2 oveq1d 
 |-  ( w = W -> ( ( # ` w ) - 1 ) = ( ( # ` W ) - 1 ) )
6 5 oveq1d 
 |-  ( w = W -> ( ( ( # ` w ) - 1 ) - x ) = ( ( ( # ` W ) - 1 ) - x ) )
7 4 6 fveq12d 
 |-  ( w = W -> ( w ` ( ( ( # ` w ) - 1 ) - x ) ) = ( W ` ( ( ( # ` W ) - 1 ) - x ) ) )
8 3 7 mpteq12dv 
 |-  ( w = W -> ( x e. ( 0 ..^ ( # ` w ) ) |-> ( w ` ( ( ( # ` w ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
9 df-reverse 
 |-  reverse = ( w e. _V |-> ( x e. ( 0 ..^ ( # ` w ) ) |-> ( w ` ( ( ( # ` w ) - 1 ) - x ) ) ) )
10 ovex 
 |-  ( 0 ..^ ( # ` W ) ) e. _V
11 10 mptex 
 |-  ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) e. _V
12 8 9 11 fvmpt 
 |-  ( W e. _V -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
13 1 12 syl 
 |-  ( W e. V -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )