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 18132
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 18130 . 2 class pmSgn
2 vd . . 3 setvar 𝑑
3 cvv 3402 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vp . . . . . . . . 9 setvar 𝑝
65cv 1636 . . . . . . . 8 class 𝑝
7 cid 5231 . . . . . . . 8 class I
86, 7cdif 3777 . . . . . . 7 class (𝑝 ∖ I )
98cdm 5324 . . . . . 6 class dom (𝑝 ∖ I )
10 cfn 8202 . . . . . 6 class Fin
119, 10wcel 2157 . . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
122cv 1636 . . . . . . 7 class 𝑑
13 csymg 18018 . . . . . . 7 class SymGrp
1412, 13cfv 6111 . . . . . 6 class (SymGrp‘𝑑)
15 cbs 16088 . . . . . 6 class Base
1614, 15cfv 6111 . . . . 5 class (Base‘(SymGrp‘𝑑))
1711, 5, 16crab 3111 . . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
184cv 1636 . . . . . . . 8 class 𝑥
19 vw . . . . . . . . . 10 setvar 𝑤
2019cv 1636 . . . . . . . . 9 class 𝑤
21 cgsu 16326 . . . . . . . . 9 class Σg
2214, 20, 21co 6884 . . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
2318, 22wceq 1637 . . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24 vs . . . . . . . . 9 setvar 𝑠
2524cv 1636 . . . . . . . 8 class 𝑠
26 c1 10232 . . . . . . . . . 10 class 1
2726cneg 10562 . . . . . . . . 9 class -1
28 chash 13357 . . . . . . . . . 10 class
2920, 28cfv 6111 . . . . . . . . 9 class (♯‘𝑤)
30 cexp 13103 . . . . . . . . 9 class
3127, 29, 30co 6884 . . . . . . . 8 class (-1↑(♯‘𝑤))
3225, 31wceq 1637 . . . . . . 7 wff 𝑠 = (-1↑(♯‘𝑤))
3323, 32wa 384 . . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
34 cpmtr 18082 . . . . . . . . 9 class pmTrsp
3512, 34cfv 6111 . . . . . . . 8 class (pmTrsp‘𝑑)
3635crn 5325 . . . . . . 7 class ran (pmTrsp‘𝑑)
3736cword 13522 . . . . . 6 class Word ran (pmTrsp‘𝑑)
3833, 19, 37wrex 3108 . . . . 5 wff 𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))
3938, 24cio 6072 . . . 4 class (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))
404, 17, 39cmpt 4934 . . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
412, 3, 40cmpt 4934 . 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
421, 41wceq 1637 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  18141
  Copyright terms: Public domain W3C validator