This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) )