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

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