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 \in Fin \land F \in T) \to F \in (P ∖ pmEven (D))$

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 \in Fin \land F \in T) \to D \in Fin$
5	3 1 2	symgtrf	$⊢ T \subseteq P$
6	5	sseli	$⊢ F \in T \to F \in P$
7	6	adantl	$⊢ (D \in Fin \land F \in T) \to F \in P$
8		eqid	$⊢ pmSgn (D) = pmSgn (D)$
9	1 3 8	psgnpmtr	$⊢ F \in T \to pmSgn (D) (F) = - 1$
10	9	adantl	$⊢ (D \in Fin \land F \in T) \to pmSgn (D) (F) = - 1$
11	1 2 8	psgnodpmr	$⊢ (D \in Fin \land F \in P \land pmSgn (D) (F) = - 1) \to F \in (P ∖ pmEven (D))$
12	4 7 10 11	syl3anc	$⊢ (D \in Fin \land F \in T) \to F \in (P ∖ pmEven (D))$

Metamath Proof Explorer