Metamath Proof Explorer

Theorem psgnfix2

Description: A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 17-Jan-2019)

		Ref	Expression
	Hypotheses	psgnfix.p	$⊢ P = {Base}_{SymGrp (N)}$
		psgnfix.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
		psgnfix.s	$⊢ S = SymGrp (N ∖ \{K\})$
		psgnfix.z	$⊢ Z = SymGrp (N)$
		psgnfix.r	$⊢ R = ran pmTrsp (N)$
	Assertion	psgnfix2	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists w \in Word R Q = \sum_{Z} w)$

Proof

Step	Hyp	Ref	Expression
1		psgnfix.p	$⊢ P = {Base}_{SymGrp (N)}$
2		psgnfix.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
3		psgnfix.s	$⊢ S = SymGrp (N ∖ \{K\})$
4		psgnfix.z	$⊢ Z = SymGrp (N)$
5		psgnfix.r	$⊢ R = ran pmTrsp (N)$
6		elrabi	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q \in P$
7	6	adantl	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to Q \in P$
8	4	fveq2i	$⊢ {Base}_{Z} = {Base}_{SymGrp (N)}$
9	1 8	eqtr4i	$⊢ P = {Base}_{Z}$
10	4 9 5	psgnfitr	$⊢ N \in Fin \to (Q \in P \leftrightarrow \exists w \in Word R Q = \sum_{Z} w)$
11	10	bicomd	$⊢ N \in Fin \to (\exists w \in Word R Q = \sum_{Z} w \leftrightarrow Q \in P)$
12	11	ad2antrr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (\exists w \in Word R Q = \sum_{Z} w \leftrightarrow Q \in P)$
13	7 12	mpbird	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to \exists w \in Word R Q = \sum_{Z} w$
14	13	ex	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists w \in Word R Q = \sum_{Z} w)$