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