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

Metamath Proof Explorer

Theorem psgnfieu

Description: A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfitr.g 
|- G = ( SymGrp ` N )
psgnfitr.p 
|- B = ( Base ` G )
psgnfitr.t 
|- T = ran ( pmTrsp ` N )
Assertion psgnfieu 
|- ( ( N e. Fin /\ Q e. B ) -> E! s E. w e. Word T ( Q = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfitr.g 
 |-  G = ( SymGrp ` N )
2 psgnfitr.p 
 |-  B = ( Base ` G )
3 psgnfitr.t 
 |-  T = ran ( pmTrsp ` N )
4 simpr 
 |-  ( ( N e. Fin /\ Q e. B ) -> Q e. B )
5 1 2 sygbasnfpfi 
 |-  ( ( N e. Fin /\ Q e. B ) -> dom ( Q \ _I ) e. Fin )
6 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
7 1 6 2 psgneldm 
 |-  ( Q e. dom ( pmSgn ` N ) <-> ( Q e. B /\ dom ( Q \ _I ) e. Fin ) )
8 4 5 7 sylanbrc 
 |-  ( ( N e. Fin /\ Q e. B ) -> Q e. dom ( pmSgn ` N ) )
9 1 3 6 psgneu 
 |-  ( Q e. dom ( pmSgn ` N ) -> E! s E. w e. Word T ( Q = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
10 8 9 syl 
 |-  ( ( N e. Fin /\ Q e. B ) -> E! s E. w e. Word T ( Q = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )