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

Definition df-sgns 31145
Description: Signum function for a structure. See also df-sgn 14650 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.)
Assertion
Ref Expression
df-sgns sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))))
Distinct variable group:   𝑥,𝑟

Detailed syntax breakdown of Definition df-sgns
StepHypRef Expression
1 csgns 31144 . 2 class sgns
2 vr . . 3 setvar 𝑟
3 cvv 3408 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1542 . . . . 5 class 𝑟
6 cbs 16760 . . . . 5 class Base
75, 6cfv 6380 . . . 4 class (Base‘𝑟)
84cv 1542 . . . . . 6 class 𝑥
9 c0g 16944 . . . . . . 7 class 0g
105, 9cfv 6380 . . . . . 6 class (0g𝑟)
118, 10wceq 1543 . . . . 5 wff 𝑥 = (0g𝑟)
12 cc0 10729 . . . . 5 class 0
13 cplt 17815 . . . . . . . 8 class lt
145, 13cfv 6380 . . . . . . 7 class (lt‘𝑟)
1510, 8, 14wbr 5053 . . . . . 6 wff (0g𝑟)(lt‘𝑟)𝑥
16 c1 10730 . . . . . 6 class 1
1716cneg 11063 . . . . . 6 class -1
1815, 16, 17cif 4439 . . . . 5 class if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)
1911, 12, 18cif 4439 . . . 4 class if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))
204, 7, 19cmpt 5135 . . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)))
212, 3, 20cmpt 5135 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))))
221, 21wceq 1543 1 wff sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))))
Colors of variables: wff setvar class
This definition is referenced by:  sgnsv  31146
  Copyright terms: Public domain W3C validator