Definition df-psgn 18699

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 18697	. 2 class pmSgn
2		vd	. . 3 setvar 𝑑
3		cvv 3409	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vp	. . . . . . . . 9 setvar 𝑝
6	5	cv 1537	. . . . . . . 8 class 𝑝
7		cid 5433	. . . . . . . 8 class I
8	6, 7	cdif 3857	. . . . . . 7 class (𝑝 ∖ I )
9	8	cdm 5528	. . . . . 6 class dom (𝑝 ∖ I )
10		cfn 8540	. . . . . 6 class Fin
11	9, 10	wcel 2111	. . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
12	2	cv 1537	. . . . . . 7 class 𝑑
13		csymg 18575	. . . . . . 7 class SymGrp
14	12, 13	cfv 6340	. . . . . 6 class (SymGrp‘𝑑)
15		cbs 16554	. . . . . 6 class Base
16	14, 15	cfv 6340	. . . . 5 class (Base‘(SymGrp‘𝑑))
17	11, 5, 16	crab 3074	. . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
18	4	cv 1537	. . . . . . . 8 class 𝑥
19		vw	. . . . . . . . . 10 setvar 𝑤
20	19	cv 1537	. . . . . . . . 9 class 𝑤
21		cgsu 16785	. . . . . . . . 9 class Σg
22	14, 20, 21	co 7156	. . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
23	18, 22	wceq 1538	. . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24		vs	. . . . . . . . 9 setvar 𝑠
25	24	cv 1537	. . . . . . . 8 class 𝑠
26		c1 10589	. . . . . . . . . 10 class 1
27	26	cneg 10922	. . . . . . . . 9 class -1
28		chash 13753	. . . . . . . . . 10 class ♯
29	20, 28	cfv 6340	. . . . . . . . 9 class (♯‘𝑤)
30		cexp 13492	. . . . . . . . 9 class ↑
31	27, 29, 30	co 7156	. . . . . . . 8 class (-1↑(♯‘𝑤))
32	25, 31	wceq 1538	. . . . . . 7 wff 𝑠 = (-1↑(♯‘𝑤))
33	23, 32	wa 399	. . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
34		cpmtr 18649	. . . . . . . . 9 class pmTrsp
35	12, 34	cfv 6340	. . . . . . . 8 class (pmTrsp‘𝑑)
36	35	crn 5529	. . . . . . 7 class ran (pmTrsp‘𝑑)
37	36	cword 13926	. . . . . 6 class Word ran (pmTrsp‘𝑑)
38	33, 19, 37	wrex 3071	. . . . 5 wff ∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
39	38, 24	cio 6297	. . . 4 class (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))
40	4, 17, 39	cmpt 5116	. . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
41	2, 3, 40	cmpt 5116	. 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
42	1, 41	wceq 1538	1 wff pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))

This definition is referenced by:  psgnfval  18708