Metamath Proof Explorer

Theorem revco

Description: Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion revco 
|- ( ( W e. Word A /\ F : A --> B ) -> ( F o. ( reverse ` W ) ) = ( reverse ` ( F o. W ) ) )

Proof

Step Hyp Ref Expression
1 wrdfn 
 |-  ( W e. Word A -> W Fn ( 0 ..^ ( # ` W ) ) )
2 1 ad2antrr 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> W Fn ( 0 ..^ ( # ` W ) ) )
3 lencl 
 |-  ( W e. Word A -> ( # ` W ) e. NN0 )
4 3 nn0zd 
 |-  ( W e. Word A -> ( # ` W ) e. ZZ )
5 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
6 4 5 syl 
 |-  ( W e. Word A -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
7 6 adantr 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
8 7 eleq2d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) )
9 8 biimpa 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ... ( ( # ` W ) - 1 ) ) )
10 fznn0sub2 
 |-  ( x e. ( 0 ... ( ( # ` W ) - 1 ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
11 9 10 syl 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
12 7 adantr 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
13 11 12 eleqtrrd 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) )
14 fvco2 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( ( # ` W ) - 1 ) - x ) ) = ( F ` ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
15 2 13 14 syl2anc 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( ( # ` W ) - 1 ) - x ) ) = ( F ` ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
16 lenco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
17 16 oveq1d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( ( # ` ( F o. W ) ) - 1 ) = ( ( # ` W ) - 1 ) )
18 17 oveq1d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( ( ( # ` ( F o. W ) ) - 1 ) - x ) = ( ( ( # ` W ) - 1 ) - x ) )
19 18 adantr 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` ( F o. W ) ) - 1 ) - x ) = ( ( ( # ` W ) - 1 ) - x ) )
20 19 fveq2d 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) = ( ( F o. W ) ` ( ( ( # ` W ) - 1 ) - x ) ) )
21 revfv 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` x ) = ( W ` ( ( ( # ` W ) - 1 ) - x ) ) )
22 21 adantlr 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` x ) = ( W ` ( ( ( # ` W ) - 1 ) - x ) ) )
23 22 fveq2d 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( F ` ( ( reverse ` W ) ` x ) ) = ( F ` ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
24 15 20 23 3eqtr4d 
 |-  ( ( ( W e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) = ( F ` ( ( reverse ` W ) ` x ) ) )
25 24 mpteq2dva 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) )
26 16 oveq2d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( 0 ..^ ( # ` ( F o. W ) ) ) = ( 0 ..^ ( # ` W ) ) )
27 26 mpteq1d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( # ` ( F o. W ) ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) )
28 revlen 
 |-  ( W e. Word A -> ( # ` ( reverse ` W ) ) = ( # ` W ) )
29 28 adantr 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` ( reverse ` W ) ) = ( # ` W ) )
30 29 oveq2d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( 0 ..^ ( # ` ( reverse ` W ) ) ) = ( 0 ..^ ( # ` W ) ) )
31 30 mpteq1d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) )
32 25 27 31 3eqtr4rd 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) = ( x e. ( 0 ..^ ( # ` ( F o. W ) ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) )
33 simpr 
 |-  ( ( W e. Word A /\ F : A --> B ) -> F : A --> B )
34 revcl 
 |-  ( W e. Word A -> ( reverse ` W ) e. Word A )
35 wrdf 
 |-  ( ( reverse ` W ) e. Word A -> ( reverse ` W ) : ( 0 ..^ ( # ` ( reverse ` W ) ) ) --> A )
36 34 35 syl 
 |-  ( W e. Word A -> ( reverse ` W ) : ( 0 ..^ ( # ` ( reverse ` W ) ) ) --> A )
37 36 adantr 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( reverse ` W ) : ( 0 ..^ ( # ` ( reverse ` W ) ) ) --> A )
38 fcompt 
 |-  ( ( F : A --> B /\ ( reverse ` W ) : ( 0 ..^ ( # ` ( reverse ` W ) ) ) --> A ) -> ( F o. ( reverse ` W ) ) = ( x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) )
39 33 37 38 syl2anc 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( F o. ( reverse ` W ) ) = ( x e. ( 0 ..^ ( # ` ( reverse ` W ) ) ) |-> ( F ` ( ( reverse ` W ) ` x ) ) ) )
40 ffun 
 |-  ( F : A --> B -> Fun F )
41 simpl 
 |-  ( ( W e. Word A /\ F : A --> B ) -> W e. Word A )
42 cofunexg 
 |-  ( ( Fun F /\ W e. Word A ) -> ( F o. W ) e. _V )
43 40 41 42 syl2an2 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) e. _V )
44 revval 
 |-  ( ( F o. W ) e. _V -> ( reverse ` ( F o. W ) ) = ( x e. ( 0 ..^ ( # ` ( F o. W ) ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) )
45 43 44 syl 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( reverse ` ( F o. W ) ) = ( x e. ( 0 ..^ ( # ` ( F o. W ) ) ) |-> ( ( F o. W ) ` ( ( ( # ` ( F o. W ) ) - 1 ) - x ) ) ) )
46 32 39 45 3eqtr4d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( F o. ( reverse ` W ) ) = ( reverse ` ( F o. W ) ) )