# Metamath Proof Explorer

## Theorem evpmss

Description: Even permutations are permutations. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
Assertion evpmss ${⊢}\mathrm{pmEven}\left({D}\right)\subseteq {P}$

### Proof

Step Hyp Ref Expression
1 evpmss.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
2 evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
3 fveq2 ${⊢}{d}={D}\to \mathrm{pmSgn}\left({d}\right)=\mathrm{pmSgn}\left({D}\right)$
4 3 cnveqd ${⊢}{d}={D}\to {\mathrm{pmSgn}\left({d}\right)}^{-1}={\mathrm{pmSgn}\left({D}\right)}^{-1}$
5 4 imaeq1d ${⊢}{d}={D}\to {\mathrm{pmSgn}\left({d}\right)}^{-1}\left[\left\{1\right\}\right]={\mathrm{pmSgn}\left({D}\right)}^{-1}\left[\left\{1\right\}\right]$
6 df-evpm ${⊢}\mathrm{pmEven}=\left({d}\in \mathrm{V}⟼{\mathrm{pmSgn}\left({d}\right)}^{-1}\left[\left\{1\right\}\right]\right)$
7 fvex ${⊢}\mathrm{pmSgn}\left({D}\right)\in \mathrm{V}$
8 7 cnvex ${⊢}{\mathrm{pmSgn}\left({D}\right)}^{-1}\in \mathrm{V}$
9 8 imaex ${⊢}{\mathrm{pmSgn}\left({D}\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{V}$
10 5 6 9 fvmpt ${⊢}{D}\in \mathrm{V}\to \mathrm{pmEven}\left({D}\right)={\mathrm{pmSgn}\left({D}\right)}^{-1}\left[\left\{1\right\}\right]$
11 cnvimass ${⊢}{\mathrm{pmSgn}\left({D}\right)}^{-1}\left[\left\{1\right\}\right]\subseteq \mathrm{dom}\mathrm{pmSgn}\left({D}\right)$
12 eqid ${⊢}\mathrm{pmSgn}\left({D}\right)=\mathrm{pmSgn}\left({D}\right)$
13 eqid ${⊢}{S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)={S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)$
14 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}$
15 1 12 13 14 psgnghm ${⊢}{D}\in \mathrm{V}\to \mathrm{pmSgn}\left({D}\right)\in \left(\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)$
16 eqid ${⊢}{\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}={\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}$
17 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)}$
18 16 17 ghmf ${⊢}\mathrm{pmSgn}\left({D}\right)\in \left(\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)\to \mathrm{pmSgn}\left({D}\right):{\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}$
19 fdm ${⊢}\mathrm{pmSgn}\left({D}\right):{\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}\to \mathrm{dom}\mathrm{pmSgn}\left({D}\right)={\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}$
20 15 18 19 3syl ${⊢}{D}\in \mathrm{V}\to \mathrm{dom}\mathrm{pmSgn}\left({D}\right)={\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}$
21 13 2 ressbasss ${⊢}{\mathrm{Base}}_{\left({S}{↾}_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left({D}\right)\right)}\subseteq {P}$
22 20 21 eqsstrdi ${⊢}{D}\in \mathrm{V}\to \mathrm{dom}\mathrm{pmSgn}\left({D}\right)\subseteq {P}$
23 11 22 sstrid ${⊢}{D}\in \mathrm{V}\to {\mathrm{pmSgn}\left({D}\right)}^{-1}\left[\left\{1\right\}\right]\subseteq {P}$
24 10 23 eqsstrd ${⊢}{D}\in \mathrm{V}\to \mathrm{pmEven}\left({D}\right)\subseteq {P}$
25 fvprc ${⊢}¬{D}\in \mathrm{V}\to \mathrm{pmEven}\left({D}\right)=\varnothing$
26 0ss ${⊢}\varnothing \subseteq {P}$
27 25 26 eqsstrdi ${⊢}¬{D}\in \mathrm{V}\to \mathrm{pmEven}\left({D}\right)\subseteq {P}$
28 24 27 pm2.61i ${⊢}\mathrm{pmEven}\left({D}\right)\subseteq {P}$