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

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 e. Fin /\ F e. T ) -> F e. ( 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 e. Fin /\ F e. T ) -> D e. Fin )
5 3 1 2 symgtrf 
 |-  T C_ P
6 5 sseli 
 |-  ( F e. T -> F e. P )
7 6 adantl 
 |-  ( ( D e. Fin /\ F e. T ) -> F e. P )
8 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
9 1 3 8 psgnpmtr 
 |-  ( F e. T -> ( ( pmSgn ` D ) ` F ) = -u 1 )
10 9 adantl 
 |-  ( ( D e. Fin /\ F e. T ) -> ( ( pmSgn ` D ) ` F ) = -u 1 )
11 1 2 8 psgnodpmr 
 |-  ( ( D e. Fin /\ F e. P /\ ( ( pmSgn ` D ) ` F ) = -u 1 ) -> F e. ( P \ ( pmEven ` D ) ) )
12 4 7 10 11 syl3anc 
 |-  ( ( D e. Fin /\ F e. T ) -> F e. ( P \ ( pmEven ` D ) ) )