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