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 e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. w e. Word T ( Q |` ( N \ { K } ) ) = ( S gsum 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 e. P | ( q ` K ) = K } = { q e. 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 e. N /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` S ) )
8	7	adantll	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` S ) )
9		diffi	|- ( N e. Fin -> ( N \ { K } ) e. Fin )
10	9	ad2antrr	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( N \ { K } ) e. Fin )
11		eqid	|- ( Base ` S ) = ( Base ` S )
12	3 11 2	psgnfitr	|- ( ( N \ { K } ) e. Fin -> ( ( Q |` ( N \ { K } ) ) e. ( Base ` S ) <-> E. w e. Word T ( Q |` ( N \ { K } ) ) = ( S gsum w ) ) )
13	10 12	syl	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( Q |` ( N \ { K } ) ) e. ( Base ` S ) <-> E. w e. Word T ( Q |` ( N \ { K } ) ) = ( S gsum w ) ) )
14	8 13	mpbid	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> E. w e. Word T ( Q |` ( N \ { K } ) ) = ( S gsum w ) )
15	14	ex	|- ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. w e. Word T ( Q |` ( N \ { K } ) ) = ( S gsum w ) ) )