Definition df-sgns 29726

Description: Signum function for a structure. See also df-sgn 13827 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.)

Assertion

Ref	Expression
df-sgns	|- sgns = ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )

Distinct variable group:   x, r

Detailed syntax breakdown of Definition df-sgns

Step	Hyp	Ref	Expression
1		csgns 29725	. 2 class sgns
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . 5 class r
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` r )
8	4	cv 1482	. . . . . 6 class x
9		c0g 16100	. . . . . . 7 class 0g
10	5, 9	cfv 5888	. . . . . 6 class ( 0g ` r )
11	8, 10	wceq 1483	. . . . 5 wff x = ( 0g ` r )
12		cc0 9936	. . . . 5 class 0
13		cplt 16941	. . . . . . . 8 class lt
14	5, 13	cfv 5888	. . . . . . 7 class ( lt ` r )
15	10, 8, 14	wbr 4653	. . . . . 6 wff ( 0g ` r ) ( lt ` r ) x
16		c1 9937	. . . . . 6 class 1
17	16	cneg 10267	. . . . . 6 class -u 1
18	15, 16, 17	cif 4086	. . . . 5 class if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 )
19	11, 12, 18	cif 4086	. . . 4 class if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) )
20	4, 7, 19	cmpt 4729	. . 3 class ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) )
21	2, 3, 20	cmpt 4729	. 2 class ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )
22	1, 21	wceq 1483	1 wff sgns = ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )

This definition is referenced by:  sgnsv  29727