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 )