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 𝑆 = ( SymGrp ‘ 𝐷 )
evpmodpmf1o.p 𝑃 = ( Base ‘ 𝑆 )
Assertion evpmodpmf1o ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( 𝑓 ∈ ( pmEven ‘ 𝐷 ) ↦ ( 𝐹 ( +g𝑆 ) 𝑓 ) ) : ( pmEven ‘ 𝐷 ) –1-1-onto→ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )

Proof

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