Definition df-psgn

Description: Define a function which takes the value 1 for even permutations and -u 1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Assertion	df-psgn	$$⊢\mathrm{pmSgn}=\left(d\in \mathrm{V}⟼\left(x\in \left\{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}⟼\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsgn	$$class\mathrm{pmSgn}$$
1		vd	$$setvard$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vp	$$setvarp$$
5		cbs	$$class\mathrm{Base}$$
6		csymg	$$class\mathrm{SymGrp}$$
7	1	cv	$$setvard$$
8	7 6	cfv	$$class\mathrm{SymGrp}\left(d\right)$$
9	8 5	cfv	$$class{\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}$$
10	4	cv	$$setvarp$$
11		cid	$$class\mathrm{I}$$
12	10 11	cdif	$$class\left(p\setminus \mathrm{I}\right)$$
13	12	cdm	$$class\mathrm{dom}\left(p\setminus \mathrm{I}\right)$$
14		cfn	$$class\mathrm{Fin}$$
15	13 14	wcel	$$wff\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
16	15 4 9	crab	$$class\left\{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
17		vs	$$setvars$$
18		vw	$$setvarw$$
19		cpmtr	$$class\mathrm{pmTrsp}$$
20	7 19	cfv	$$class\mathrm{pmTrsp}\left(d\right)$$
21	20	crn	$$class\mathrm{ran}\mathrm{pmTrsp}\left(d\right)$$
22	21	cword	$$class\mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)$$
23	3	cv	$$setvarx$$
24		cgsu	$$class{\Sigma }_{𝑔}$$
25	18	cv	$$setvarw$$
26	8 25 24	co	$$class\left({\sum }_{\mathrm{SymGrp}\left(d\right)},w\right)$$
27	23 26	wceq	$$wffx={\sum }_{\mathrm{SymGrp}\left(d\right)}w$$
28	17	cv	$$setvars$$
29		c1	$$class1$$
30	29	cneg	$$class-1$$
31		cexp	$$class^$$
32		chash	$$class\left|.\right|$$
33	25 32	cfv	$$class\left|w\right|$$
34	30 33 31	co	$$class{\left(-1\right)}^{\left|w\right|}$$
35	28 34	wceq	$$wffs={\left(-1\right)}^{\left|w\right|}$$
36	27 35	wa	$$wff\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)$$
37	36 18 22	wrex	$$wff\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)$$
38	37 17	cio	$$class\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)$$
39	3 16 38	cmpt	$$class\left(x\in \left\{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}⟼\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\right)$$
40	1 2 39	cmpt	$$class\left(d\in \mathrm{V}⟼\left(x\in \left\{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}⟼\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\right)\right)$$
41	0 40	wceq	$$wff\mathrm{pmSgn}=\left(d\in \mathrm{V}⟼\left(x\in \left\{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(d\right)}|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}⟼\left(\iota s|\exists w\in \mathrm{Word}\mathrm{ran}\mathrm{pmTrsp}\left(d\right)\left(x={\sum }_{\mathrm{SymGrp}\left(d\right)}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)\right)\right)$$