Theorem gsmtrcl

Description: The group sum of transpositions of a finite set is a permutation, see also psgneldm2i . (Contributed by AV, 19-Jan-2019)

	Ref	Expression
Hypotheses	gsmtrcl.s	|- S = ( SymGrp ` N )
	gsmtrcl.b	|- B = ( Base ` S )
	gsmtrcl.t	|- T = ran ( pmTrsp ` N )
Assertion	gsmtrcl	|- ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsmtrcl.s	|- S = ( SymGrp ` N )
2		gsmtrcl.b	|- B = ( Base ` S )
3		gsmtrcl.t	|- T = ran ( pmTrsp ` N )
4		eqid	|- ( pmSgn ` N ) = ( pmSgn ` N )
5	1 3 4	psgneldm2i	|- ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. dom ( pmSgn ` N ) )
6	1 4 2	psgneldm	|- ( ( S gsum W ) e. dom ( pmSgn ` N ) <-> ( ( S gsum W ) e. B /\ dom ( ( S gsum W ) \ _I ) e. Fin ) )
7		ax-1	|- ( ( S gsum W ) e. B -> ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. B ) )
8	7	adantr	|- ( ( ( S gsum W ) e. B /\ dom ( ( S gsum W ) \ _I ) e. Fin ) -> ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. B ) )
9	6 8	sylbi	|- ( ( S gsum W ) e. dom ( pmSgn ` N ) -> ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. B ) )
10	5 9	mpcom	|- ( ( N e. Fin /\ W e. Word T ) -> ( S gsum W ) e. B )