# Metamath Proof Explorer

## Theorem psgnodpm

Description: A permutation which is odd (i.e. not even) has 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 psgnodpm ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {N}\left({F}\right)=-1$

### 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 eldif ${⊢}{F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)↔\left({F}\in {P}\wedge ¬{F}\in \mathrm{pmEven}\left({D}\right)\right)$
5 simpr ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to {F}\in {P}$
6 5 a1d ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({N}\left({F}\right)=1\to {F}\in {P}\right)$
7 6 ancrd ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({N}\left({F}\right)=1\to \left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$
8 1 2 3 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)$
9 8 adantr ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({F}\in \mathrm{pmEven}\left({D}\right)↔\left({F}\in {P}\wedge {N}\left({F}\right)=1\right)\right)$
10 7 9 sylibrd ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({N}\left({F}\right)=1\to {F}\in \mathrm{pmEven}\left({D}\right)\right)$
11 10 con3d ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left(¬{F}\in \mathrm{pmEven}\left({D}\right)\to ¬{N}\left({F}\right)=1\right)$
12 11 impr ${⊢}\left({D}\in \mathrm{Fin}\wedge \left({F}\in {P}\wedge ¬{F}\in \mathrm{pmEven}\left({D}\right)\right)\right)\to ¬{N}\left({F}\right)=1$
13 4 12 sylan2b ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to ¬{N}\left({F}\right)=1$
14 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}$
15 1 3 14 psgnghm2 ${⊢}{D}\in \mathrm{Fin}\to {N}\in \left({S}\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)$
16 15 adantr ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {N}\in \left({S}\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)$
17 14 cnmsgnbas ${⊢}\left\{1,-1\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)}$
18 2 17 ghmf ${⊢}{N}\in \left({S}\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}\right)\right)\to {N}:{P}⟶\left\{1,-1\right\}$
19 16 18 syl ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {N}:{P}⟶\left\{1,-1\right\}$
20 eldifi ${⊢}{F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\to {F}\in {P}$
21 20 adantl ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {F}\in {P}$
22 19 21 ffvelrnd ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {N}\left({F}\right)\in \left\{1,-1\right\}$
23 fvex ${⊢}{N}\left({F}\right)\in \mathrm{V}$
24 23 elpr ${⊢}{N}\left({F}\right)\in \left\{1,-1\right\}↔\left({N}\left({F}\right)=1\vee {N}\left({F}\right)=-1\right)$
25 22 24 sylib ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to \left({N}\left({F}\right)=1\vee {N}\left({F}\right)=-1\right)$
26 orel1 ${⊢}¬{N}\left({F}\right)=1\to \left(\left({N}\left({F}\right)=1\vee {N}\left({F}\right)=-1\right)\to {N}\left({F}\right)=-1\right)$
27 13 25 26 sylc ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)\right)\to {N}\left({F}\right)=-1$