Theorem psgnevpm

Description: A permutation which is even has 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	psgnevpm	|- ( ( D e. Fin /\ F e. ( pmEven ` D ) ) -> ( 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	1 2 3	psgnevpmb	|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )
5	4	simplbda	|- ( ( D e. Fin /\ F e. ( pmEven ` D ) ) -> ( N ` F ) = 1 )