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 ‘ 𝐷 ) ) )