Metamath Proof Explorer

Theorem psgnval

Description: Value of the permutation sign function. (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 psgnval 
|- ( P e. dom N -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

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 eqeq1 
 |-  ( t = P -> ( t = ( G gsum w ) <-> P = ( G gsum w ) ) )
5 4 anbi1d 
 |-  ( t = P -> ( ( t = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
6 5 rexbidv 
 |-  ( t = P -> ( E. w e. Word T ( t = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
7 6 iotabidv 
 |-  ( t = P -> ( iota s E. w e. Word T ( t = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
8 eqid 
 |-  ( Base ` G ) = ( Base ` G )
9 eqid 
 |-  { x e. ( Base ` G ) | dom ( x \ _I ) e. Fin } = { x e. ( Base ` G ) | dom ( x \ _I ) e. Fin }
10 1 8 9 3 psgnfn 
 |-  N Fn { x e. ( Base ` G ) | dom ( x \ _I ) e. Fin }
11 10 fndmi 
 |-  dom N = { x e. ( Base ` G ) | dom ( x \ _I ) e. Fin }
12 1 8 11 2 3 psgnfval 
 |-  N = ( t e. dom N |-> ( iota s E. w e. Word T ( t = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
13 iotaex 
 |-  ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) e. _V
14 7 12 13 fvmpt 
 |-  ( P e. dom N -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )