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 17680
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 17678 . 2 class pmSgn
2 vd . . 3 setvar 𝑑
3 cvv 3172 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vp . . . . . . . . 9 setvar 𝑝
65cv 1473 . . . . . . . 8 class 𝑝
7 cid 4938 . . . . . . . 8 class I
86, 7cdif 3536 . . . . . . 7 class (𝑝 ∖ I )
98cdm 5028 . . . . . 6 class dom (𝑝 ∖ I )
10 cfn 7818 . . . . . 6 class Fin
119, 10wcel 1976 . . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
122cv 1473 . . . . . . 7 class 𝑑
13 csymg 17566 . . . . . . 7 class SymGrp
1412, 13cfv 5790 . . . . . 6 class (SymGrp‘𝑑)
15 cbs 15641 . . . . . 6 class Base
1614, 15cfv 5790 . . . . 5 class (Base‘(SymGrp‘𝑑))
1711, 5, 16crab 2899 . . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
184cv 1473 . . . . . . . 8 class 𝑥
19 vw . . . . . . . . . 10 setvar 𝑤
2019cv 1473 . . . . . . . . 9 class 𝑤
21 cgsu 15870 . . . . . . . . 9 class Σg
2214, 20, 21co 6527 . . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
2318, 22wceq 1474 . . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24 vs . . . . . . . . 9 setvar 𝑠
2524cv 1473 . . . . . . . 8 class 𝑠
26 c1 9793 . . . . . . . . . 10 class 1
2726cneg 10118 . . . . . . . . 9 class -1
28 chash 12934 . . . . . . . . . 10 class #
2920, 28cfv 5790 . . . . . . . . 9 class (#‘𝑤)
30 cexp 12677 . . . . . . . . 9 class
3127, 29, 30co 6527 . . . . . . . 8 class (-1↑(#‘𝑤))
3225, 31wceq 1474 . . . . . . 7 wff 𝑠 = (-1↑(#‘𝑤))
3323, 32wa 382 . . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
34 cpmtr 17630 . . . . . . . . 9 class pmTrsp
3512, 34cfv 5790 . . . . . . . 8 class (pmTrsp‘𝑑)
3635crn 5029 . . . . . . 7 class ran (pmTrsp‘𝑑)
3736cword 13092 . . . . . 6 class Word ran (pmTrsp‘𝑑)
3833, 19, 37wrex 2896 . . . . 5 wff 𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
3938, 24cio 5752 . . . 4 class (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))
404, 17, 39cmpt 4637 . . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))
412, 3, 40cmpt 4637 . 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))))
421, 41wceq 1474 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  17689
  Copyright terms: Public domain W3C validator