Metamath Proof Explorer

Theorem psgnfix1

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

		Ref	Expression
	Hypotheses	psgnfix.p	$⊢ P = {Base}_{SymGrp (N)}$
		psgnfix.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
		psgnfix.s	$⊢ S = SymGrp (N ∖ \{K\})$
	Assertion	psgnfix1	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists w \in Word T {Q ↾}_{(N ∖ \{K\})} = \sum_{S} 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		eqid	$⊢ \{q \in P \| q (K) = K\} = \{q \in P \| q (K) = K\}$
5	3	fveq2i	$⊢ {Base}_{S} = {Base}_{SymGrp (N ∖ \{K\})}$
6		eqid	$⊢ N ∖ \{K\} = N ∖ \{K\}$
7	1 4 5 6	symgfixelsi	$⊢ (K \in N \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{S}$
8	7	adantll	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{S}$
9		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
10	9	ad2antrr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to N ∖ \{K\} \in Fin$
11		eqid	$⊢ {Base}_{S} = {Base}_{S}$
12	3 11 2	psgnfitr	$⊢ N ∖ \{K\} \in Fin \to ({Q ↾}_{(N ∖ \{K\})} \in {Base}_{S} \leftrightarrow \exists w \in Word T {Q ↾}_{(N ∖ \{K\})} = \sum_{S} w)$
13	10 12	syl	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ({Q ↾}_{(N ∖ \{K\})} \in {Base}_{S} \leftrightarrow \exists w \in Word T {Q ↾}_{(N ∖ \{K\})} = \sum_{S} w)$
14	8 13	mpbid	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to \exists w \in Word T {Q ↾}_{(N ∖ \{K\})} = \sum_{S} w$
15	14	ex	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists w \in Word T {Q ↾}_{(N ∖ \{K\})} = \sum_{S} w)$