Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sgns Structured version   Unicode version

Definition df-sgns 26188
Description: Signum function for a structure. See also df-sgn 12575 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
StepHypRef Expression
1 csgns 26187 . 2  class sgns
2 vr . . 3  setvar  r
3 cvv 2971 . . 3  class  _V
4 vx . . . 4  setvar  x
52cv 1368 . . . . 5  class  r
6 cbs 14173 . . . . 5  class  Base
75, 6cfv 5417 . . . 4  class  ( Base `  r )
84cv 1368 . . . . . 6  class  x
9 c0g 14377 . . . . . . 7  class  0g
105, 9cfv 5417 . . . . . 6  class  ( 0g
`  r )
118, 10wceq 1369 . . . . 5  wff  x  =  ( 0g `  r
)
12 cc0 9281 . . . . 5  class  0
13 cplt 15110 . . . . . . . 8  class  lt
145, 13cfv 5417 . . . . . . 7  class  ( lt
`  r )
1510, 8, 14wbr 4291 . . . . . 6  wff  ( 0g
`  r ) ( lt `  r ) x
16 c1 9282 . . . . . 6  class  1
1716cneg 9595 . . . . . 6  class  -u 1
1815, 16, 17cif 3790 . . . . 5  class  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
)
1911, 12, 18cif 3790 . . . 4  class  if ( x  =  ( 0g
`  r ) ,  0 ,  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
) )
204, 7, 19cmpt 4349 . . 3  class  ( x  e.  ( Base `  r
)  |->  if ( x  =  ( 0g `  r ) ,  0 ,  if ( ( 0g `  r ) ( lt `  r
) x ,  1 ,  -u 1 ) ) )
212, 3, 20cmpt 4349 . 2  class  ( r  e.  _V  |->  ( x  e.  ( Base `  r
)  |->  if ( x  =  ( 0g `  r ) ,  0 ,  if ( ( 0g `  r ) ( lt `  r
) x ,  1 ,  -u 1 ) ) ) )
221, 21wceq 1369 1  wff sgns  =  (
r  e.  _V  |->  ( x  e.  ( Base `  r )  |->  if ( x  =  ( 0g
`  r ) ,  0 ,  if ( ( 0g `  r
) ( lt `  r ) x ,  1 ,  -u 1
) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sgnsv  26189
  Copyright terms: Public domain W3C validator