Metamath Proof Explorer


Theorem psgnfn

Description: Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnfn.g
|- G = ( SymGrp ` D )
psgnfn.b
|- B = ( Base ` G )
psgnfn.f
|- F = { p e. B | dom ( p \ _I ) e. Fin }
psgnfn.n
|- N = ( pmSgn ` D )
Assertion psgnfn
|- N Fn F

Proof

Step Hyp Ref Expression
1 psgnfn.g
 |-  G = ( SymGrp ` D )
2 psgnfn.b
 |-  B = ( Base ` G )
3 psgnfn.f
 |-  F = { p e. B | dom ( p \ _I ) e. Fin }
4 psgnfn.n
 |-  N = ( pmSgn ` D )
5 iotaex
 |-  ( iota s E. w e. Word ran ( pmTrsp ` D ) ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) e. _V
6 eqid
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
7 1 2 3 6 4 psgnfval
 |-  N = ( x e. F |-> ( iota s E. w e. Word ran ( pmTrsp ` D ) ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
8 5 7 fnmpti
 |-  N Fn F