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=\mathrm{SymGrp}\left(D\right)$$
	psgnfn.b	$$⊢B={\mathrm{Base}}_G$$
	psgnfn.f	$$⊢F=\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
	psgnfn.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnfn	$$⊢NFnF$$

Proof

Step	Hyp	Ref	Expression
1		psgnfn.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
2		psgnfn.b	$$⊢B={\mathrm{Base}}_G$$
3		psgnfn.f	$$⊢F=\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
4		psgnfn.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
5		iotaex	$$⊢\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(D\right)\left(x={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\in \mathrm{V}$$
6		eqid	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(D\right)=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
7	1 2 3 6 4	psgnfval	$$⊢N=\left(x\in F⟼\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(D\right)\left(x={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\right)$$
8	5 7	fnmpti	$$⊢NFnF$$