Metamath Proof Explorer


Theorem psgnevpmb

Description: A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s S = SymGrp D
evpmss.p P = Base S
psgnevpmb.n N = pmSgn D
Assertion psgnevpmb D Fin F pmEven D F P N F = 1

Proof

Step Hyp Ref Expression
1 evpmss.s S = SymGrp D
2 evpmss.p P = Base S
3 psgnevpmb.n N = pmSgn D
4 elex D Fin D V
5 fveq2 d = D pmSgn d = pmSgn D
6 5 3 eqtr4di d = D pmSgn d = N
7 6 cnveqd d = D pmSgn d -1 = N -1
8 7 imaeq1d d = D pmSgn d -1 1 = N -1 1
9 df-evpm pmEven = d V pmSgn d -1 1
10 3 fvexi N V
11 10 cnvex N -1 V
12 11 imaex N -1 1 V
13 8 9 12 fvmpt D V pmEven D = N -1 1
14 4 13 syl D Fin pmEven D = N -1 1
15 14 eleq2d D Fin F pmEven D F N -1 1
16 eqid mulGrp fld 𝑠 1 1 = mulGrp fld 𝑠 1 1
17 1 3 16 psgnghm2 D Fin N S GrpHom mulGrp fld 𝑠 1 1
18 eqid Base mulGrp fld 𝑠 1 1 = Base mulGrp fld 𝑠 1 1
19 2 18 ghmf N S GrpHom mulGrp fld 𝑠 1 1 N : P Base mulGrp fld 𝑠 1 1
20 17 19 syl D Fin N : P Base mulGrp fld 𝑠 1 1
21 ffn N : P Base mulGrp fld 𝑠 1 1 N Fn P
22 fniniseg N Fn P F N -1 1 F P N F = 1
23 20 21 22 3syl D Fin F N -1 1 F P N F = 1
24 15 23 bitrd D Fin F pmEven D F P N F = 1