Metamath Proof Explorer

Definition df-psgn

Description: Define a function which takes the value 1 for even permutations and -u 1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Assertion df-psgn ⊢ pmSgn = d ∈ V ⟼ x ∈ p ∈ Base SymGrp ⁡ d | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsgn class pmSgn
1 vd setvar d
2 cvv class V
3 vx setvar x
4 vp setvar p
5 cbs class Base
6 csymg class SymGrp
7 1 cv setvar d
8 7 6 cfv class SymGrp ⁡ d
9 8 5 cfv class Base SymGrp ⁡ d
10 4 cv setvar p
11 cid class I
12 10 11 cdif class p ∖ I
13 12 cdm class dom ⁡ p ∖ I
14 cfn class Fin
15 13 14 wcel wff dom ⁡ p ∖ I ∈ Fin
16 15 4 9 crab class p ∈ Base SymGrp ⁡ d | dom ⁡ p ∖ I ∈ Fin
17 vs setvar s
18 vw setvar w
19 cpmtr class pmTrsp
20 7 19 cfv class pmTrsp ⁡ d
21 20 crn class ran ⁡ pmTrsp ⁡ d
22 21 cword class Word ran ⁡ pmTrsp ⁡ d
23 3 cv setvar x
24 cgsu class Σ𝑔
25 18 cv setvar w
26 8 25 24 co class ∑ SymGrp ⁡ d w
27 23 26 wceq wff x = ∑ SymGrp ⁡ d w
28 17 cv setvar s
29 c1 class 1
30 29 cneg class -1
31 cexp class ^
32 chash class .
33 25 32 cfv class w
34 30 33 31 co class − 1 w
35 28 34 wceq wff s = − 1 w
36 27 35 wa wff x = ∑ SymGrp ⁡ d w ∧ s = − 1 w
37 36 18 22 wrex wff ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w
38 37 17 cio class ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w
39 3 16 38 cmpt class x ∈ p ∈ Base SymGrp ⁡ d | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w
40 1 2 39 cmpt class d ∈ V ⟼ x ∈ p ∈ Base SymGrp ⁡ d | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w
41 0 40 wceq wff pmSgn = d ∈ V ⟼ x ∈ p ∈ Base SymGrp ⁡ d | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ d x = ∑ SymGrp ⁡ d w ∧ s = − 1 w