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

Metamath Proof Explorer

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 )