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

Metamath Proof Explorer

Theorem psgnvalfi

Description: Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfvalfi.g 
|- G = ( SymGrp ` D )
psgnfvalfi.b 
|- B = ( Base ` G )
psgnfvalfi.t 
|- T = ran ( pmTrsp ` D )
psgnfvalfi.n 
|- N = ( pmSgn ` D )
Assertion psgnvalfi 
|- ( ( D e. Fin /\ P e. B ) -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

Proof

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