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 e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. w e. Word R Q = ( Z 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		psgnfix.z	|- Z = ( SymGrp ` N )
5		psgnfix.r	|- R = ran ( pmTrsp ` N )
6		elrabi	|- ( Q e. { q e. P | ( q ` K ) = K } -> Q e. P )
7	6	adantl	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> Q e. P )
8	4	fveq2i	|- ( Base ` Z ) = ( Base ` ( SymGrp ` N ) )
9	1 8	eqtr4i	|- P = ( Base ` Z )
10	4 9 5	psgnfitr	|- ( N e. Fin -> ( Q e. P <-> E. w e. Word R Q = ( Z gsum w ) ) )
11	10	bicomd	|- ( N e. Fin -> ( E. w e. Word R Q = ( Z gsum w ) <-> Q e. P ) )
12	11	ad2antrr	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( E. w e. Word R Q = ( Z gsum w ) <-> Q e. P ) )
13	7 12	mpbird	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> E. w e. Word R Q = ( Z gsum w ) )
14	13	ex	|- ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. w e. Word R Q = ( Z gsum w ) ) )