Theorem psgnevpm

Description: A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	evpmss.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	evpmss.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
	psgnevpmb.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnevpm	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) → ( 𝑁 ‘ 𝐹 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		evpmss.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		evpmss.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
3		psgnevpmb.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4	1 2 3	psgnevpmb	⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
5	4	simplbda	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) → ( 𝑁 ‘ 𝐹 ) = 1 )