# 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 } ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`