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 |
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 |