Metamath Proof Explorer

Theorem symgtrinv

Description: To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Hypotheses symgtrinv.t 
|- T = ran ( pmTrsp ` D )
symgtrinv.g 
|- G = ( SymGrp ` D )
symgtrinv.i 
|- I = ( invg ` G )
Assertion symgtrinv 
|- ( ( D e. V /\ W e. Word T ) -> ( I ` ( G gsum W ) ) = ( G gsum ( reverse ` W ) ) )

Proof

Step Hyp Ref Expression
1 symgtrinv.t 
 |-  T = ran ( pmTrsp ` D )
2 symgtrinv.g 
 |-  G = ( SymGrp ` D )
3 symgtrinv.i 
 |-  I = ( invg ` G )
4 2 symggrp 
 |-  ( D e. V -> G e. Grp )
5 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
6 5 3 invoppggim 
 |-  ( G e. Grp -> I e. ( G GrpIso ( oppG ` G ) ) )
7 gimghm 
 |-  ( I e. ( G GrpIso ( oppG ` G ) ) -> I e. ( G GrpHom ( oppG ` G ) ) )
8 ghmmhm 
 |-  ( I e. ( G GrpHom ( oppG ` G ) ) -> I e. ( G MndHom ( oppG ` G ) ) )
9 4 6 7 8 4syl 
 |-  ( D e. V -> I e. ( G MndHom ( oppG ` G ) ) )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 1 2 10 symgtrf 
 |-  T C_ ( Base ` G )
12 sswrd 
 |-  ( T C_ ( Base ` G ) -> Word T C_ Word ( Base ` G ) )
13 11 12 ax-mp 
 |-  Word T C_ Word ( Base ` G )
14 13 sseli 
 |-  ( W e. Word T -> W e. Word ( Base ` G ) )
15 10 gsumwmhm 
 |-  ( ( I e. ( G MndHom ( oppG ` G ) ) /\ W e. Word ( Base ` G ) ) -> ( I ` ( G gsum W ) ) = ( ( oppG ` G ) gsum ( I o. W ) ) )
16 9 14 15 syl2an 
 |-  ( ( D e. V /\ W e. Word T ) -> ( I ` ( G gsum W ) ) = ( ( oppG ` G ) gsum ( I o. W ) ) )
17 10 3 grpinvf 
 |-  ( G e. Grp -> I : ( Base ` G ) --> ( Base ` G ) )
18 4 17 syl 
 |-  ( D e. V -> I : ( Base ` G ) --> ( Base ` G ) )
19 wrdf 
 |-  ( W e. Word T -> W : ( 0 ..^ ( # ` W ) ) --> T )
20 19 adantl 
 |-  ( ( D e. V /\ W e. Word T ) -> W : ( 0 ..^ ( # ` W ) ) --> T )
21 fss 
 |-  ( ( W : ( 0 ..^ ( # ` W ) ) --> T /\ T C_ ( Base ` G ) ) -> W : ( 0 ..^ ( # ` W ) ) --> ( Base ` G ) )
22 20 11 21 sylancl 
 |-  ( ( D e. V /\ W e. Word T ) -> W : ( 0 ..^ ( # ` W ) ) --> ( Base ` G ) )
23 fco 
 |-  ( ( I : ( Base ` G ) --> ( Base ` G ) /\ W : ( 0 ..^ ( # ` W ) ) --> ( Base ` G ) ) -> ( I o. W ) : ( 0 ..^ ( # ` W ) ) --> ( Base ` G ) )
24 18 22 23 syl2an2r 
 |-  ( ( D e. V /\ W e. Word T ) -> ( I o. W ) : ( 0 ..^ ( # ` W ) ) --> ( Base ` G ) )
25 24 ffnd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( I o. W ) Fn ( 0 ..^ ( # ` W ) ) )
26 20 ffnd 
 |-  ( ( D e. V /\ W e. Word T ) -> W Fn ( 0 ..^ ( # ` W ) ) )
27 fvco2 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I o. W ) ` x ) = ( I ` ( W ` x ) ) )
28 26 27 sylan 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I o. W ) ` x ) = ( I ` ( W ` x ) ) )
29 20 ffvelrnda 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` x ) e. T )
30 11 29 sseldi 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` x ) e. ( Base ` G ) )
31 2 10 3 symginv 
 |-  ( ( W ` x ) e. ( Base ` G ) -> ( I ` ( W ` x ) ) = `' ( W ` x ) )
32 30 31 syl 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( I ` ( W ` x ) ) = `' ( W ` x ) )
33 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
34 33 1 pmtrfcnv 
 |-  ( ( W ` x ) e. T -> `' ( W ` x ) = ( W ` x ) )
35 29 34 syl 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> `' ( W ` x ) = ( W ` x ) )
36 28 32 35 3eqtrd 
 |-  ( ( ( D e. V /\ W e. Word T ) /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I o. W ) ` x ) = ( W ` x ) )
37 25 26 36 eqfnfvd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( I o. W ) = W )
38 37 oveq2d 
 |-  ( ( D e. V /\ W e. Word T ) -> ( ( oppG ` G ) gsum ( I o. W ) ) = ( ( oppG ` G ) gsum W ) )
39 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
40 4 39 syl 
 |-  ( D e. V -> G e. Mnd )
41 10 5 gsumwrev 
 |-  ( ( G e. Mnd /\ W e. Word ( Base ` G ) ) -> ( ( oppG ` G ) gsum W ) = ( G gsum ( reverse ` W ) ) )
42 40 14 41 syl2an 
 |-  ( ( D e. V /\ W e. Word T ) -> ( ( oppG ` G ) gsum W ) = ( G gsum ( reverse ` W ) ) )
43 16 38 42 3eqtrd 
 |-  ( ( D e. V /\ W e. Word T ) -> ( I ` ( G gsum W ) ) = ( G gsum ( reverse ` W ) ) )