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