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

Definition df-psgn 17957
 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 17955 . 2 class pmSgn
2 vd . . 3 setvar 𝑑
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vp . . . . . . . . 9 setvar 𝑝
65cv 1522 . . . . . . . 8 class 𝑝
7 cid 5052 . . . . . . . 8 class I
86, 7cdif 3604 . . . . . . 7 class (𝑝 ∖ I )
98cdm 5143 . . . . . 6 class dom (𝑝 ∖ I )
10 cfn 7997 . . . . . 6 class Fin
119, 10wcel 2030 . . . . 5 wff dom (𝑝 ∖ I ) ∈ Fin
122cv 1522 . . . . . . 7 class 𝑑
13 csymg 17843 . . . . . . 7 class SymGrp
1412, 13cfv 5926 . . . . . 6 class (SymGrp‘𝑑)
15 cbs 15904 . . . . . 6 class Base
1614, 15cfv 5926 . . . . 5 class (Base‘(SymGrp‘𝑑))
1711, 5, 16crab 2945 . . . 4 class {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin}
184cv 1522 . . . . . . . 8 class 𝑥
19 vw . . . . . . . . . 10 setvar 𝑤
2019cv 1522 . . . . . . . . 9 class 𝑤
21 cgsu 16148 . . . . . . . . 9 class Σg
2214, 20, 21co 6690 . . . . . . . 8 class ((SymGrp‘𝑑) Σg 𝑤)
2318, 22wceq 1523 . . . . . . 7 wff 𝑥 = ((SymGrp‘𝑑) Σg 𝑤)
24 vs . . . . . . . . 9 setvar 𝑠
2524cv 1522 . . . . . . . 8 class 𝑠
26 c1 9975 . . . . . . . . . 10 class 1
2726cneg 10305 . . . . . . . . 9 class -1
28 chash 13157 . . . . . . . . . 10 class #
2920, 28cfv 5926 . . . . . . . . 9 class (#‘𝑤)
30 cexp 12900 . . . . . . . . 9 class
3127, 29, 30co 6690 . . . . . . . 8 class (-1↑(#‘𝑤))
3225, 31wceq 1523 . . . . . . 7 wff 𝑠 = (-1↑(#‘𝑤))
3323, 32wa 383 . . . . . 6 wff (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
34 cpmtr 17907 . . . . . . . . 9 class pmTrsp
3512, 34cfv 5926 . . . . . . . 8 class (pmTrsp‘𝑑)
3635crn 5144 . . . . . . 7 class ran (pmTrsp‘𝑑)
3736cword 13323 . . . . . 6 class Word ran (pmTrsp‘𝑑)
3833, 19, 37wrex 2942 . . . . 5 wff 𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))
3938, 24cio 5887 . . . 4 class (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))
404, 17, 39cmpt 4762 . . 3 class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))
412, 3, 40cmpt 4762 . 2 class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))))
421, 41wceq 1523 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  17966
 Copyright terms: Public domain W3C validator