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 ) ) ) |