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

Definition df-psgn 16838
 Description: Define a function which takes the value for even permutations and for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.)
Assertion
Ref Expression
df-psgn pmSgn Word pmTrsp g
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-psgn
StepHypRef Expression
1 cpsgn 16836 . 2 pmSgn
2 vd . . 3
3 cvv 3058 . . 3
4 vx . . . 4
5 vp . . . . . . . . 9
65cv 1404 . . . . . . . 8
7 cid 4732 . . . . . . . 8
86, 7cdif 3410 . . . . . . 7
98cdm 4822 . . . . . 6
10 cfn 7553 . . . . . 6
119, 10wcel 1842 . . . . 5
122cv 1404 . . . . . . 7
13 csymg 16724 . . . . . . 7
1412, 13cfv 5568 . . . . . 6
15 cbs 14839 . . . . . 6
1614, 15cfv 5568 . . . . 5
1711, 5, 16crab 2757 . . . 4
184cv 1404 . . . . . . . 8
19 vw . . . . . . . . . 10
2019cv 1404 . . . . . . . . 9
21 cgsu 15053 . . . . . . . . 9 g
2214, 20, 21co 6277 . . . . . . . 8 g
2318, 22wceq 1405 . . . . . . 7 g
24 vs . . . . . . . . 9
2524cv 1404 . . . . . . . 8
26 c1 9522 . . . . . . . . . 10
2726cneg 9841 . . . . . . . . 9
28 chash 12450 . . . . . . . . . 10
2920, 28cfv 5568 . . . . . . . . 9
30 cexp 12208 . . . . . . . . 9
3127, 29, 30co 6277 . . . . . . . 8
3225, 31wceq 1405 . . . . . . 7
3323, 32wa 367 . . . . . 6 g
34 cpmtr 16788 . . . . . . . . 9 pmTrsp
3512, 34cfv 5568 . . . . . . . 8 pmTrsp
3635crn 4823 . . . . . . 7 pmTrsp
3736cword 12581 . . . . . 6 Word pmTrsp
3833, 19, 37wrex 2754 . . . . 5 Word pmTrsp g
3938, 24cio 5530 . . . 4 Word pmTrsp g
404, 17, 39cmpt 4452 . . 3 Word pmTrsp g
412, 3, 40cmpt 4452 . 2 Word pmTrsp g
421, 41wceq 1405 1 pmSgn Word pmTrsp g
 Colors of variables: wff setvar class This definition is referenced by:  psgnfval  16847
 Copyright terms: Public domain W3C validator