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 syl6eq
 |-  ( ( ( 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 syl6eq
 |-  ( ( ( 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 syl6eqr
 |-  ( ( 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 syl6eqr
 |-  ( ( 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 ) ) )