Definition df-psgn 17911

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

Assertion

Ref	Expression
df-psgn	⊢ pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))))

Distinct variable group:   𝑥,𝑠,𝑤,𝑑,𝑝

Detailed syntax breakdown of Definition df-psgn

Step	Hyp	Ref	Expression
1		cpsgn 17909	. 2 class pmSgn
2		vd	. . 3 setvar 𝑑
3		cvv 3200	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vp	. . . . . . . . 9 setvar 𝑝
6	5	cv 1482	. . . . . . . 8 class 𝑝
7		cid 5023	. . . . . . . 8 class I
8	6, 7	cdif 3571	. . . . . . 7 class (𝑝 ∖ I )
9	8	cdm 5114	. . . . . 6 class dom (𝑝 ∖ I )
10		cfn 7955	. . . . . 6 class Fin
11	9, 10	wcel 1990	. . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
12	2	cv 1482	. . . . . . 7 class 𝑑
13		csymg 17797	. . . . . . 7 class SymGrp
14	12, 13	cfv 5888	. . . . . 6 class (SymGrp‘𝑑)
15		cbs 15857	. . . . . 6 class Base
16	14, 15	cfv 5888	. . . . 5 class (Base‘(SymGrp‘𝑑))
17	11, 5, 16	crab 2916	. . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
18	4	cv 1482	. . . . . . . 8 class 𝑥
19		vw	. . . . . . . . . 10 setvar 𝑤
20	19	cv 1482	. . . . . . . . 9 class 𝑤
21		cgsu 16101	. . . . . . . . 9 class Σg
22	14, 20, 21	co 6650	. . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
23	18, 22	wceq 1483	. . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24		vs	. . . . . . . . 9 setvar 𝑠
25	24	cv 1482	. . . . . . . 8 class 𝑠
26		c1 9937	. . . . . . . . . 10 class 1
27	26	cneg 10267	. . . . . . . . 9 class -1
28		chash 13117	. . . . . . . . . 10 class #
29	20, 28	cfv 5888	. . . . . . . . 9 class (#‘𝑤)
30		cexp 12860	. . . . . . . . 9 class ↑
31	27, 29, 30	co 6650	. . . . . . . 8 class (-1↑(#‘𝑤))
32	25, 31	wceq 1483	. . . . . . 7 wff 𝑠 = (-1↑(#‘𝑤))
33	23, 32	wa 384	. . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
34		cpmtr 17861	. . . . . . . . 9 class pmTrsp
35	12, 34	cfv 5888	. . . . . . . 8 class (pmTrsp‘𝑑)
36	35	crn 5115	. . . . . . 7 class ran (pmTrsp‘𝑑)
37	36	cword 13291	. . . . . 6 class Word ran (pmTrsp‘𝑑)
38	33, 19, 37	wrex 2913	. . . . 5 wff ∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
39	38, 24	cio 5849	. . . 4 class (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))
40	4, 17, 39	cmpt 4729	. . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))
41	2, 3, 40	cmpt 4729	. 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))))
42	1, 41	wceq 1483	1 wff pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))))

This definition is referenced by:  psgnfval  17920