Metamath Proof Explorer

Definition df-sgns

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgns 
 |-  sgns
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Base ` r )
7 3 cv 
 |-  x
8 c0g 
 |-  0g
9 5 8 cfv 
 |-  ( 0g ` r )
10 7 9 wceq 
 |-  x = ( 0g ` r )
11 cc0 
 |-  0
12 cplt 
 |-  lt
13 5 12 cfv 
 |-  ( lt ` r )
14 9 7 13 wbr 
 |-  ( 0g ` r ) ( lt ` r ) x
15 c1 
 |-  1
16 15 cneg 
 |-  -u 1
17 14 15 16 cif 
 |-  if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 )
18 10 11 17 cif 
 |-  if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) )
19 3 6 18 cmpt 
 |-  ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) )
20 1 2 19 cmpt 
 |-  ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )
21 0 20 wceq 
 |-  sgns = ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )