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 sselid
 |-  ( ( ( 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 4 grpmndd
 |-  ( D e. V -> G e. Mnd )
40 10 5 gsumwrev
 |-  ( ( G e. Mnd /\ W e. Word ( Base ` G ) ) -> ( ( oppG ` G ) gsum W ) = ( G gsum ( reverse ` W ) ) )
41 39 14 40 syl2an
 |-  ( ( D e. V /\ W e. Word T ) -> ( ( oppG ` G ) gsum W ) = ( G gsum ( reverse ` W ) ) )
42 16 38 41 3eqtrd
 |-  ( ( D e. V /\ W e. Word T ) -> ( I ` ( G gsum W ) ) = ( G gsum ( reverse ` W ) ) )