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 ⊢ S = SymGrp ⁡ D
evpmss.p ⊢ P = Base S
psgnevpmb.n ⊢ N = pmSgn ⁡ D
Assertion psgnevpm ⊢ D ∈ Fin ∧ F ∈ 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 ∈ Fin → F ∈ pmEven ⁡ D ↔ F ∈ P ∧ N ⁡ F = 1
5 4 simplbda ⊢ D ∈ Fin ∧ F ∈ pmEven ⁡ D → N ⁡ F = 1