This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )