# 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}=\mathrm{SymGrp}\left({D}\right)$
evpmodpmf1o.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
Assertion evpmodpmf1o ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to \left({f}\in \mathrm{pmEven}\left({D}\right)⟼{F}{+}_{{S}}{f}\right):\mathrm{pmEven}\left({D}\right)\underset{1-1 onto}{⟶}{P}\setminus \mathrm{pmEven}\left({D}\right)$

### Proof

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