Metamath Proof Explorer

Theorem pmtrodpm

Description: A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmodpmf1o.s ⊢ S = SymGrp ⁡ D
evpmodpmf1o.p ⊢ P = Base S
pmtrodpm.t ⊢ T = ran ⁡ pmTrsp ⁡ D
Assertion pmtrodpm ⊢ D ∈ Fin ∧ F ∈ T → F ∈ P ∖ pmEven ⁡ D

Proof

Step Hyp Ref Expression
1 evpmodpmf1o.s ⊢ S = SymGrp ⁡ D
2 evpmodpmf1o.p ⊢ P = Base S
3 pmtrodpm.t ⊢ T = ran ⁡ pmTrsp ⁡ D
4 simpl ⊢ D ∈ Fin ∧ F ∈ T → D ∈ Fin
5 3 1 2 symgtrf ⊢ T ⊆ P
6 5 sseli ⊢ F ∈ T → F ∈ P
7 6 adantl ⊢ D ∈ Fin ∧ F ∈ T → F ∈ P
8 eqid ⊢ pmSgn ⁡ D = pmSgn ⁡ D
9 1 3 8 psgnpmtr ⊢ F ∈ T → pmSgn ⁡ D ⁡ F = − 1
10 9 adantl ⊢ D ∈ Fin ∧ F ∈ T → pmSgn ⁡ D ⁡ F = − 1
11 1 2 8 psgnodpmr ⊢ D ∈ Fin ∧ F ∈ P ∧ pmSgn ⁡ D ⁡ F = − 1 → F ∈ P ∖ pmEven ⁡ D
12 4 7 10 11 syl3anc ⊢ D ∈ Fin ∧ F ∈ T → F ∈ P ∖ pmEven ⁡ D