Metamath Proof Explorer

Theorem revrev

Description: Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 revcl 
 |-  ( W e. Word A -> ( reverse ` W ) e. Word A )
2 revcl 
 |-  ( ( reverse ` W ) e. Word A -> ( reverse ` ( reverse ` W ) ) e. Word A )
3 wrdf 
 |-  ( ( reverse ` ( reverse ` W ) ) e. Word A -> ( reverse ` ( reverse ` W ) ) : ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) --> A )
4 ffn 
 |-  ( ( reverse ` ( reverse ` W ) ) : ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) --> A -> ( reverse ` ( reverse ` W ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) )
5 1 2 3 4 4syl 
 |-  ( W e. Word A -> ( reverse ` ( reverse ` W ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) )
6 revlen 
 |-  ( ( reverse ` W ) e. Word A -> ( # ` ( reverse ` ( reverse ` W ) ) ) = ( # ` ( reverse ` W ) ) )
7 1 6 syl 
 |-  ( W e. Word A -> ( # ` ( reverse ` ( reverse ` W ) ) ) = ( # ` ( reverse ` W ) ) )
8 revlen 
 |-  ( W e. Word A -> ( # ` ( reverse ` W ) ) = ( # ` W ) )
9 7 8 eqtrd 
 |-  ( W e. Word A -> ( # ` ( reverse ` ( reverse ` W ) ) ) = ( # ` W ) )
10 9 oveq2d 
 |-  ( W e. Word A -> ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) = ( 0 ..^ ( # ` W ) ) )
11 10 fneq2d 
 |-  ( W e. Word A -> ( ( reverse ` ( reverse ` W ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( reverse ` W ) ) ) ) <-> ( reverse ` ( reverse ` W ) ) Fn ( 0 ..^ ( # ` W ) ) ) )
12 5 11 mpbid 
 |-  ( W e. Word A -> ( reverse ` ( reverse ` W ) ) Fn ( 0 ..^ ( # ` W ) ) )
13 wrdfn 
 |-  ( W e. Word A -> W Fn ( 0 ..^ ( # ` W ) ) )
14 simpr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) )
15 8 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` ( reverse ` W ) ) = ( # ` W ) )
16 15 oveq2d 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( reverse ` W ) ) ) = ( 0 ..^ ( # ` W ) ) )
17 14 16 eleqtrrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) )
18 revfv 
 |-  ( ( ( reverse ` W ) e. Word A /\ x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) ) -> ( ( reverse ` ( reverse ` W ) ) ` x ) = ( ( reverse ` W ) ` ( ( ( # ` ( reverse ` W ) ) - 1 ) - x ) ) )
19 1 17 18 syl2an2r 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` ( reverse ` W ) ) ` x ) = ( ( reverse ` W ) ` ( ( ( # ` ( reverse ` W ) ) - 1 ) - x ) ) )
20 15 oveq1d 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` ( reverse ` W ) ) - 1 ) = ( ( # ` W ) - 1 ) )
21 20 fvoveq1d 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( ( ( # ` ( reverse ` W ) ) - 1 ) - x ) ) = ( ( reverse ` W ) ` ( ( ( # ` W ) - 1 ) - x ) ) )
22 lencl 
 |-  ( W e. Word A -> ( # ` W ) e. NN0 )
23 22 nn0zd 
 |-  ( W e. Word A -> ( # ` W ) e. ZZ )
24 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
25 23 24 syl 
 |-  ( W e. Word A -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
26 25 eleq2d 
 |-  ( W e. Word A -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) )
27 26 biimpa 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ... ( ( # ` W ) - 1 ) ) )
28 fznn0sub2 
 |-  ( x e. ( 0 ... ( ( # ` W ) - 1 ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
29 27 28 syl 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
30 25 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
31 29 30 eleqtrrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) )
32 revfv 
 |-  ( ( W e. Word A /\ ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( ( ( # ` W ) - 1 ) - x ) ) = ( W ` ( ( ( # ` W ) - 1 ) - ( ( ( # ` W ) - 1 ) - x ) ) ) )
33 31 32 syldan 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( ( ( # ` W ) - 1 ) - x ) ) = ( W ` ( ( ( # ` W ) - 1 ) - ( ( ( # ` W ) - 1 ) - x ) ) ) )
34 peano2zm 
 |-  ( ( # ` W ) e. ZZ -> ( ( # ` W ) - 1 ) e. ZZ )
35 23 34 syl 
 |-  ( W e. Word A -> ( ( # ` W ) - 1 ) e. ZZ )
36 35 zcnd 
 |-  ( W e. Word A -> ( ( # ` W ) - 1 ) e. CC )
37 elfzoelz 
 |-  ( x e. ( 0 ..^ ( # ` W ) ) -> x e. ZZ )
38 37 zcnd 
 |-  ( x e. ( 0 ..^ ( # ` W ) ) -> x e. CC )
39 nncan 
 |-  ( ( ( ( # ` W ) - 1 ) e. CC /\ x e. CC ) -> ( ( ( # ` W ) - 1 ) - ( ( ( # ` W ) - 1 ) - x ) ) = x )
40 36 38 39 syl2an 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - ( ( ( # ` W ) - 1 ) - x ) ) = x )
41 40 fveq2d 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - ( ( ( # ` W ) - 1 ) - x ) ) ) = ( W ` x ) )
42 33 41 eqtrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( ( ( # ` W ) - 1 ) - x ) ) = ( W ` x ) )
43 21 42 eqtrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( ( ( # ` ( reverse ` W ) ) - 1 ) - x ) ) = ( W ` x ) )
44 19 43 eqtrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` ( reverse ` W ) ) ` x ) = ( W ` x ) )
45 12 13 44 eqfnfvd 
 |-  ( W e. Word A -> ( reverse ` ( reverse ` W ) ) = W )