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 eqtrdi ⊢ ( ( ( 𝐷 ∈ 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 eqtrdi ⊢ ( ( ( 𝐷 ∈ 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 eqtr4di ⊢ ( ( 𝐷 ∈ 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 eqtr4di ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( ( 𝑓 ∈ ( pmEven ‘ 𝐷 ) ↦ ( 𝐹 ( +g ‘ 𝑆 ) 𝑓 ) ) ∘ ( 𝑔 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ↦ ( ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) ( +g ‘ 𝑆 ) 𝑔 ) ) ) = ( I ↾ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) )
104 37 70 88 103 fcof1od ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( 𝑓 ∈ ( pmEven ‘ 𝐷 ) ↦ ( 𝐹 ( +g ‘ 𝑆 ) 𝑓 ) ) : ( pmEven ‘ 𝐷 ) –1-1-onto→ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )