This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evpmodpmf1o

Description: The function for performing an even permutation after a fixed odd permutation is one to one onto all odd permutations. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmodpmf1o.s 
|- S = ( SymGrp ` D )
evpmodpmf1o.p 
|- P = ( Base ` S )
Assertion evpmodpmf1o 
|- ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) : ( pmEven ` D ) -1-1-onto-> ( P \ ( pmEven ` D ) ) )

Proof

Step Hyp Ref Expression
1 evpmodpmf1o.s 
 |-  S = ( SymGrp ` D )
2 evpmodpmf1o.p 
 |-  P = ( Base ` S )
3 simpll 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> D e. Fin )
4 1 symggrp 
 |-  ( D e. Fin -> S e. Grp )
5 4 ad2antrr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> S e. Grp )
6 eldifi 
 |-  ( F e. ( P \ ( pmEven ` D ) ) -> F e. P )
7 6 ad2antlr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> F e. P )
8 1 2 evpmss 
 |-  ( pmEven ` D ) C_ P
9 8 sseli 
 |-  ( f e. ( pmEven ` D ) -> f e. P )
10 9 adantl 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> f e. P )
11 eqid 
 |-  ( +g ` S ) = ( +g ` S )
12 2 11 grpcl 
 |-  ( ( S e. Grp /\ F e. P /\ f e. P ) -> ( F ( +g ` S ) f ) e. P )
13 5 7 10 12 syl3anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( F ( +g ` S ) f ) e. P )
14 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
15 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
16 1 14 15 psgnghm2 
 |-  ( D e. Fin -> ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
17 16 ad2antrr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
18 prex 
 |-  { 1 , -u 1 } e. _V
19 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
20 cnfldmul 
 |-  x. = ( .r ` CCfld )
21 19 20 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
22 15 21 ressplusg 
 |-  ( { 1 , -u 1 } e. _V -> x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
23 18 22 ax-mp 
 |-  x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
24 2 11 23 ghmlin 
 |-  ( ( ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P /\ f e. P ) -> ( ( pmSgn ` D ) ` ( F ( +g ` S ) f ) ) = ( ( ( pmSgn ` D ) ` F ) x. ( ( pmSgn ` D ) ` f ) ) )
25 17 7 10 24 syl3anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` ( F ( +g ` S ) f ) ) = ( ( ( pmSgn ` D ) ` F ) x. ( ( pmSgn ` D ) ` f ) ) )
26 1 2 14 psgnodpm 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` F ) = -u 1 )
27 26 adantr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` F ) = -u 1 )
28 1 2 14 psgnevpm 
 |-  ( ( D e. Fin /\ f e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` f ) = 1 )
29 28 adantlr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` f ) = 1 )
30 27 29 oveq12d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( pmSgn ` D ) ` F ) x. ( ( pmSgn ` D ) ` f ) ) = ( -u 1 x. 1 ) )
31 ax-1cn 
 |-  1 e. CC
32 31 mulm1i 
 |-  ( -u 1 x. 1 ) = -u 1
33 30 32 eqtrdi 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( pmSgn ` D ) ` F ) x. ( ( pmSgn ` D ) ` f ) ) = -u 1 )
34 25 33 eqtrd 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` ( F ( +g ` S ) f ) ) = -u 1 )
35 1 2 14 psgnodpmr 
 |-  ( ( D e. Fin /\ ( F ( +g ` S ) f ) e. P /\ ( ( pmSgn ` D ) ` ( F ( +g ` S ) f ) ) = -u 1 ) -> ( F ( +g ` S ) f ) e. ( P \ ( pmEven ` D ) ) )
36 3 13 34 35 syl3anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( F ( +g ` S ) f ) e. ( P \ ( pmEven ` D ) ) )
37 36 fmpttd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) : ( pmEven ` D ) --> ( P \ ( pmEven ` D ) ) )
38 4 ad2antrr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> S e. Grp )
39 eqid 
 |-  ( invg ` S ) = ( invg ` S )
40 2 39 grpinvcl 
 |-  ( ( S e. Grp /\ F e. P ) -> ( ( invg ` S ) ` F ) e. P )
41 4 6 40 syl2an 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( invg ` S ) ` F ) e. P )
42 41 adantr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( invg ` S ) ` F ) e. P )
43 eldifi 
 |-  ( g e. ( P \ ( pmEven ` D ) ) -> g e. P )
44 43 adantl 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> g e. P )
45 2 11 grpcl 
 |-  ( ( S e. Grp /\ ( ( invg ` S ) ` F ) e. P /\ g e. P ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. P )
46 38 42 44 45 syl3anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. P )
47 16 ad2antrr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
48 2 11 23 ghmlin 
 |-  ( ( ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ ( ( invg ` S ) ` F ) e. P /\ g e. P ) -> ( ( pmSgn ` D ) ` ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = ( ( ( pmSgn ` D ) ` ( ( invg ` S ) ` F ) ) x. ( ( pmSgn ` D ) ` g ) ) )
49 47 42 44 48 syl3anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = ( ( ( pmSgn ` D ) ` ( ( invg ` S ) ` F ) ) x. ( ( pmSgn ` D ) ` g ) ) )
50 1 2 39 symginv 
 |-  ( F e. P -> ( ( invg ` S ) ` F ) = `' F )
51 6 50 syl 
 |-  ( F e. ( P \ ( pmEven ` D ) ) -> ( ( invg ` S ) ` F ) = `' F )
52 51 ad2antlr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( invg ` S ) ` F ) = `' F )
53 52 fveq2d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` ( ( invg ` S ) ` F ) ) = ( ( pmSgn ` D ) ` `' F ) )
54 1 2 14 psgnodpm 
 |-  ( ( D e. Fin /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` g ) = -u 1 )
55 54 adantlr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` g ) = -u 1 )
56 53 55 oveq12d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( pmSgn ` D ) ` ( ( invg ` S ) ` F ) ) x. ( ( pmSgn ` D ) ` g ) ) = ( ( ( pmSgn ` D ) ` `' F ) x. -u 1 ) )
57 simpll 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> D e. Fin )
58 6 ad2antlr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> F e. P )
59 1 14 2 psgninv 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( pmSgn ` D ) ` `' F ) = ( ( pmSgn ` D ) ` F ) )
60 57 58 59 syl2anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` `' F ) = ( ( pmSgn ` D ) ` F ) )
61 26 adantr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` F ) = -u 1 )
62 60 61 eqtrd 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` `' F ) = -u 1 )
63 62 oveq1d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( pmSgn ` D ) ` `' F ) x. -u 1 ) = ( -u 1 x. -u 1 ) )
64 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
65 63 64 eqtrdi 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( pmSgn ` D ) ` `' F ) x. -u 1 ) = 1 )
66 49 56 65 3eqtrd 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = 1 )
67 1 2 14 psgnevpmb 
 |-  ( D e. Fin -> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. ( pmEven ` D ) <-> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. P /\ ( ( pmSgn ` D ) ` ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = 1 ) ) )
68 67 ad2antrr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. ( pmEven ` D ) <-> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. P /\ ( ( pmSgn ` D ) ` ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = 1 ) ) )
69 46 66 68 mpbir2and 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) e. ( pmEven ` D ) )
70 69 fmpttd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) : ( P \ ( pmEven ` D ) ) --> ( pmEven ` D ) )
71 eqidd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) = ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) )
72 eqidd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) )
73 oveq2 
 |-  ( g = ( F ( +g ` S ) f ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) = ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) )
74 36 71 72 73 fmptco 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) o. ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) ) = ( f e. ( pmEven ` D ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) ) )
75 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
76 2 11 75 39 grplinv 
 |-  ( ( S e. Grp /\ F e. P ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) F ) = ( 0g ` S ) )
77 5 7 76 syl2anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) F ) = ( 0g ` S ) )
78 77 oveq1d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) F ) ( +g ` S ) f ) = ( ( 0g ` S ) ( +g ` S ) f ) )
79 41 adantr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( invg ` S ) ` F ) e. P )
80 2 11 grpass 
 |-  ( ( S e. Grp /\ ( ( ( invg ` S ) ` F ) e. P /\ F e. P /\ f e. P ) ) -> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) F ) ( +g ` S ) f ) = ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) )
81 5 79 7 10 80 syl13anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( ( invg ` S ) ` F ) ( +g ` S ) F ) ( +g ` S ) f ) = ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) )
82 2 11 75 grplid 
 |-  ( ( S e. Grp /\ f e. P ) -> ( ( 0g ` S ) ( +g ` S ) f ) = f )
83 5 10 82 syl2anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( 0g ` S ) ( +g ` S ) f ) = f )
84 78 81 83 3eqtr3d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ f e. ( pmEven ` D ) ) -> ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) = f )
85 84 mpteq2dva 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( f e. ( pmEven ` D ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) ( F ( +g ` S ) f ) ) ) = ( f e. ( pmEven ` D ) |-> f ) )
86 74 85 eqtrd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) o. ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) ) = ( f e. ( pmEven ` D ) |-> f ) )
87 mptresid 
 |-  ( _I |` ( pmEven ` D ) ) = ( f e. ( pmEven ` D ) |-> f )
88 86 87 eqtr4di 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) o. ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) ) = ( _I |` ( pmEven ` D ) ) )
89 oveq2 
 |-  ( f = ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) -> ( F ( +g ` S ) f ) = ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) )
90 69 72 71 89 fmptco 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) o. ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) ) = ( g e. ( P \ ( pmEven ` D ) ) |-> ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) ) )
91 2 11 75 39 grprinv 
 |-  ( ( S e. Grp /\ F e. P ) -> ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) = ( 0g ` S ) )
92 4 6 91 syl2an 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) = ( 0g ` S ) )
93 92 oveq1d 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) ( +g ` S ) g ) = ( ( 0g ` S ) ( +g ` S ) g ) )
94 93 adantr 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) ( +g ` S ) g ) = ( ( 0g ` S ) ( +g ` S ) g ) )
95 2 11 grpass 
 |-  ( ( S e. Grp /\ ( F e. P /\ ( ( invg ` S ) ` F ) e. P /\ g e. P ) ) -> ( ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) ( +g ` S ) g ) = ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) )
96 38 58 42 44 95 syl13anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( F ( +g ` S ) ( ( invg ` S ) ` F ) ) ( +g ` S ) g ) = ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) )
97 2 11 75 grplid 
 |-  ( ( S e. Grp /\ g e. P ) -> ( ( 0g ` S ) ( +g ` S ) g ) = g )
98 38 44 97 syl2anc 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( ( 0g ` S ) ( +g ` S ) g ) = g )
99 94 96 98 3eqtr3d 
 |-  ( ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) /\ g e. ( P \ ( pmEven ` D ) ) ) -> ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) = g )
100 99 mpteq2dva 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( g e. ( P \ ( pmEven ` D ) ) |-> ( F ( +g ` S ) ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) ) = ( g e. ( P \ ( pmEven ` D ) ) |-> g ) )
101 90 100 eqtrd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) o. ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) ) = ( g e. ( P \ ( pmEven ` D ) ) |-> g ) )
102 mptresid 
 |-  ( _I |` ( P \ ( pmEven ` D ) ) ) = ( g e. ( P \ ( pmEven ` D ) ) |-> g )
103 101 102 eqtr4di 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) o. ( g e. ( P \ ( pmEven ` D ) ) |-> ( ( ( invg ` S ) ` F ) ( +g ` S ) g ) ) ) = ( _I |` ( P \ ( pmEven ` D ) ) ) )
104 37 70 88 103 fcof1od 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( f e. ( pmEven ` D ) |-> ( F ( +g ` S ) f ) ) : ( pmEven ` D ) -1-1-onto-> ( P \ ( pmEven ` D ) ) )