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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
evpmodpmf1o.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
pmtrodpm.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
Assertion pmtrodpm ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 evpmodpmf1o.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 evpmodpmf1o.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 pmtrodpm.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
4 simpl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇 ) → 𝐷 ∈ Fin )
5 3 1 2 symgtrf ⊢ 𝑇 ⊆ 𝑃
6 5 sseli ⊢ ( 𝐹 ∈ 𝑇 → 𝐹 ∈ 𝑃 )
7 6 adantl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑃 )
8 eqid ⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
9 1 3 8 psgnpmtr ⊢ ( 𝐹 ∈ 𝑇 → ( ( pmSgn ‘ 𝐷 ) ‘ 𝐹 ) = - 1 )
10 9 adantl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇 ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝐹 ) = - 1 )
11 1 2 8 psgnodpmr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ ( ( pmSgn ‘ 𝐷 ) ‘ 𝐹 ) = - 1 ) → 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )
12 4 7 10 11 syl3anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )