Metamath Proof Explorer

Theorem revlen

Description: The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revlen 
|- ( W e. Word A -> ( # ` ( reverse ` W ) ) = ( # ` W ) )

Proof

Step Hyp Ref Expression
1 revval 
 |-  ( W e. Word A -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
2 1 fveq2d 
 |-  ( W e. Word A -> ( # ` ( reverse ` W ) ) = ( # ` ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ) )
3 wrdf 
 |-  ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
4 3 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
5 simpr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) )
6 lencl 
 |-  ( W e. Word A -> ( # ` W ) e. NN0 )
7 6 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN0 )
8 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
9 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
10 7 8 9 3syl 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
11 5 10 eleqtrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ... ( ( # ` W ) - 1 ) ) )
12 fznn0sub2 
 |-  ( x e. ( 0 ... ( ( # ` W ) - 1 ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
13 11 12 syl 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
14 13 10 eleqtrrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) )
15 4 14 ffvelrnd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) e. A )
16 15 fmpttd 
 |-  ( W e. Word A -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) : ( 0 ..^ ( # ` W ) ) --> A )
17 ffn 
 |-  ( ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) : ( 0 ..^ ( # ` W ) ) --> A -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) Fn ( 0 ..^ ( # ` W ) ) )
18 hashfn 
 |-  ( ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) Fn ( 0 ..^ ( # ` W ) ) -> ( # ` ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ) = ( # ` ( 0 ..^ ( # ` W ) ) ) )
19 16 17 18 3syl 
 |-  ( W e. Word A -> ( # ` ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) ) = ( # ` ( 0 ..^ ( # ` W ) ) ) )
20 hashfzo0 
 |-  ( ( # ` W ) e. NN0 -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
21 6 20 syl 
 |-  ( W e. Word A -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
22 2 19 21 3eqtrd 
 |-  ( W e. Word A -> ( # ` ( reverse ` W ) ) = ( # ` W ) )