# 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}=\mathrm{SymGrp}\left({D}\right)$
evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
psgnevpmb.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
Assertion psgnevpmb ${⊢}{D}\in \mathrm{Fin}\to \left({F}\in \mathrm{pmEven}\left({D}\right)↔\left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$

### Proof

Step Hyp Ref Expression
1 evpmss.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
2 evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
3 psgnevpmb.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
4 elex ${⊢}{D}\in \mathrm{Fin}\to {D}\in \mathrm{V}$
5 fveq2 ${⊢}{d}={D}\to \mathrm{pmSgn}\left({d}\right)=\mathrm{pmSgn}\left({D}\right)$
6 5 3 syl6eqr ${⊢}{d}={D}\to \mathrm{pmSgn}\left({d}\right)={N}$
7 6 cnveqd ${⊢}{d}={D}\to {\mathrm{pmSgn}\left({d}\right)}^{-1}={{N}}^{-1}$
8 7 imaeq1d ${⊢}{d}={D}\to {\mathrm{pmSgn}\left({d}\right)}^{-1}\left[\left\{1\right\}\right]={{N}}^{-1}\left[\left\{1\right\}\right]$
9 df-evpm ${⊢}\mathrm{pmEven}=\left({d}\in \mathrm{V}⟼{\mathrm{pmSgn}\left({d}\right)}^{-1}\left[\left\{1\right\}\right]\right)$
10 3 fvexi ${⊢}{N}\in \mathrm{V}$
11 10 cnvex ${⊢}{{N}}^{-1}\in \mathrm{V}$
12 11 imaex ${⊢}{{N}}^{-1}\left[\left\{1\right\}\right]\in \mathrm{V}$
13 8 9 12 fvmpt ${⊢}{D}\in \mathrm{V}\to \mathrm{pmEven}\left({D}\right)={{N}}^{-1}\left[\left\{1\right\}\right]$
14 4 13 syl ${⊢}{D}\in \mathrm{Fin}\to \mathrm{pmEven}\left({D}\right)={{N}}^{-1}\left[\left\{1\right\}\right]$
15 14 eleq2d ${⊢}{D}\in \mathrm{Fin}\to \left({F}\in \mathrm{pmEven}\left({D}\right)↔{F}\in {{N}}^{-1}\left[\left\{1\right\}\right]\right)$
16 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}$
17 1 3 16 psgnghm2 ${⊢}{D}\in \mathrm{Fin}\to {N}\in \left({S}\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)$
18 eqid ${⊢}{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}$
19 2 18 ghmf ${⊢}{N}\in \left({S}\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)\to {N}:{P}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}$
20 17 19 syl ${⊢}{D}\in \mathrm{Fin}\to {N}:{P}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}$
21 ffn ${⊢}{N}:{P}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}\to {N}Fn{P}$
22 fniniseg ${⊢}{N}Fn{P}\to \left({F}\in {{N}}^{-1}\left[\left\{1\right\}\right]↔\left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$
23 20 21 22 3syl ${⊢}{D}\in \mathrm{Fin}\to \left({F}\in {{N}}^{-1}\left[\left\{1\right\}\right]↔\left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$
24 15 23 bitrd ${⊢}{D}\in \mathrm{Fin}\to \left({F}\in \mathrm{pmEven}\left({D}\right)↔\left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$