Theorem psgnevpm

Description: A permutation which is 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	psgnevpm	$$⊢\left(D\in \mathrm{Fin}\wedge F\in \mathrm{pmEven}\left(D\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	1 2 3	psgnevpmb	$$⊢D\in \mathrm{Fin}\to \left(F\in \mathrm{pmEven}\left(D\right)\leftrightarrow \left(F\in P\wedge N\left(F\right)=1\right)\right)$$
5	4	simplbda	$$⊢\left(D\in \mathrm{Fin}\wedge F\in \mathrm{pmEven}\left(D\right)\right)\to N\left(F\right)=1$$