Theorem psgneldm2i

Description: A sequence of transpositions describes a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	psgnval.g	|- G = ( SymGrp ` D )
	psgnval.t	|- T = ran ( pmTrsp ` D )
	psgnval.n	|- N = ( pmSgn ` D )
Assertion	psgneldm2i	|- ( ( D e. V /\ W e. Word T ) -> ( G gsum W ) e. dom N )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	|- G = ( SymGrp ` D )
2		psgnval.t	|- T = ran ( pmTrsp ` D )
3		psgnval.n	|- N = ( pmSgn ` D )
4		eqid	|- ( G gsum W ) = ( G gsum W )
5		oveq2	|- ( w = W -> ( G gsum w ) = ( G gsum W ) )
6	5	rspceeqv	|- ( ( W e. Word T /\ ( G gsum W ) = ( G gsum W ) ) -> E. w e. Word T ( G gsum W ) = ( G gsum w ) )
7	4 6	mpan2	|- ( W e. Word T -> E. w e. Word T ( G gsum W ) = ( G gsum w ) )
8	1 2 3	psgneldm2	|- ( D e. V -> ( ( G gsum W ) e. dom N <-> E. w e. Word T ( G gsum W ) = ( G gsum w ) ) )
9	8	biimpar	|- ( ( D e. V /\ E. w e. Word T ( G gsum W ) = ( G gsum w ) ) -> ( G gsum W ) e. dom N )
10	7 9	sylan2	|- ( ( D e. V /\ W e. Word T ) -> ( G gsum W ) e. dom N )