MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-psgn Structured version   Visualization version   GIF version

Definition df-psgn 18550
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
StepHypRef Expression
1 cpsgn 18548 . 2 class pmSgn
2 vd . . 3 setvar 𝑑
3 cvv 3495 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vp . . . . . . . . 9 setvar 𝑝
65cv 1527 . . . . . . . 8 class 𝑝
7 cid 5453 . . . . . . . 8 class I
86, 7cdif 3932 . . . . . . 7 class (𝑝 ∖ I )
98cdm 5549 . . . . . 6 class dom (𝑝 ∖ I )
10 cfn 8498 . . . . . 6 class Fin
119, 10wcel 2105 . . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
122cv 1527 . . . . . . 7 class 𝑑
13 csymg 18435 . . . . . . 7 class SymGrp
1412, 13cfv 6349 . . . . . 6 class (SymGrp‘𝑑)
15 cbs 16473 . . . . . 6 class Base
1614, 15cfv 6349 . . . . 5 class (Base‘(SymGrp‘𝑑))
1711, 5, 16crab 3142 . . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
184cv 1527 . . . . . . . 8 class 𝑥
19 vw . . . . . . . . . 10 setvar 𝑤
2019cv 1527 . . . . . . . . 9 class 𝑤
21 cgsu 16704 . . . . . . . . 9 class Σg
2214, 20, 21co 7145 . . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
2318, 22wceq 1528 . . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24 vs . . . . . . . . 9 setvar 𝑠
2524cv 1527 . . . . . . . 8 class 𝑠
26 c1 10527 . . . . . . . . . 10 class 1
2726cneg 10860 . . . . . . . . 9 class -1
28 chash 13680 . . . . . . . . . 10 class
2920, 28cfv 6349 . . . . . . . . 9 class (♯‘𝑤)
30 cexp 13419 . . . . . . . . 9 class
3127, 29, 30co 7145 . . . . . . . 8 class (-1↑(♯‘𝑤))
3225, 31wceq 1528 . . . . . . 7 wff 𝑠 = (-1↑(♯‘𝑤))
3323, 32wa 396 . . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
34 cpmtr 18500 . . . . . . . . 9 class pmTrsp
3512, 34cfv 6349 . . . . . . . 8 class (pmTrsp‘𝑑)
3635crn 5550 . . . . . . 7 class ran (pmTrsp‘𝑑)
3736cword 13851 . . . . . 6 class Word ran (pmTrsp‘𝑑)
3833, 19, 37wrex 3139 . . . . 5 wff 𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
3938, 24cio 6306 . . . 4 class (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))
404, 17, 39cmpt 5138 . . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
412, 3, 40cmpt 5138 . 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
421, 41wceq 1528 1 wff pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
Colors of variables: wff setvar class
This definition is referenced by:  psgnfval  18559
  Copyright terms: Public domain W3C validator