df-psgn - Metamath Proof Explorer

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

Definition df-psgn 17911

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 $/\$

**Detailed syntax breakdown of Definition df-psgn**
Step	Hyp	Ref	Expression
1		cpsgn 17909	. 2 pmSgn
2		vd	. . 3
3		cvv 3200	. . 3
4		vx	. . . 4
5		vp	. . . . . . . . 9
6	5	cv 1482	. . . . . . . 8
7		cid 5023	. . . . . . . 8
8	6, 7	cdif 3571	. . . . . . 7 $\$
9	8	cdm 5114	. . . . . 6 $\$
10		cfn 7955	. . . . . 6
11	9, 10	wcel 1990	. . . . 5 $\$
12	2	cv 1482	. . . . . . 7
13		csymg 17797	. . . . . . 7
14	12, 13	cfv 5888	. . . . . 6
15		cbs 15857	. . . . . 6
16	14, 15	cfv 5888	. . . . 5
17	11, 5, 16	crab 2916	. . . 4 $\$
18	4	cv 1482	. . . . . . . 8
19		vw	. . . . . . . . . 10
20	19	cv 1482	. . . . . . . . 9
21		cgsu 16101	. . . . . . . . 9 _g
22	14, 20, 21	co 6650	. . . . . . . 8 _g
23	18, 22	wceq 1483	. . . . . . 7 _g
24		vs	. . . . . . . . 9
25	24	cv 1482	. . . . . . . 8
26		c1 9937	. . . . . . . . . 10
27	26	cneg 10267	. . . . . . . . 9
28		chash 13117	. . . . . . . . . 10
29	20, 28	cfv 5888	. . . . . . . . 9
30		cexp 12860	. . . . . . . . 9
31	27, 29, 30	co 6650	. . . . . . . 8
32	25, 31	wceq 1483	. . . . . . 7
33	23, 32	wa 384	. . . . . 6 _g $/\$
34		cpmtr 17861	. . . . . . . . 9 pmTrsp
35	12, 34	cfv 5888	. . . . . . . 8 pmTrsp
36	35	crn 5115	. . . . . . 7 pmTrsp
37	36	cword 13291	. . . . . 6 Word pmTrsp
38	33, 19, 37	wrex 2913	. . . . 5 Word pmTrsp _g $/\$
39	38, 24	cio 5849	. . . 4 Word pmTrsp _g $/\$
40	4, 17, 39	cmpt 4729	. . 3 $\$ Word pmTrsp _g $/\$
41	2, 3, 40	cmpt 4729	. 2 $\$ Word pmTrsp _g $/\$
42	1, 41	wceq 1483	1 pmSgn $\$ Word pmTrsp _g $/\$

Colors of variables: wff setvar class

This definition is referenced by: psgnfval 17920