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 29854
Description: Signum function for a structure. See also df-sgn 13871 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 29853 . 2 class sgns
2 vr . . 3 setvar 𝑟
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1522 . . . . 5 class 𝑟
6 cbs 15904 . . . . 5 class Base
75, 6cfv 5926 . . . 4 class (Base‘𝑟)
84cv 1522 . . . . . 6 class 𝑥
9 c0g 16147 . . . . . . 7 class 0g
105, 9cfv 5926 . . . . . 6 class (0g𝑟)
118, 10wceq 1523 . . . . 5 wff 𝑥 = (0g𝑟)
12 cc0 9974 . . . . 5 class 0
13 cplt 16988 . . . . . . . 8 class lt
145, 13cfv 5926 . . . . . . 7 class (lt‘𝑟)
1510, 8, 14wbr 4685 . . . . . 6 wff (0g𝑟)(lt‘𝑟)𝑥
16 c1 9975 . . . . . 6 class 1
1716cneg 10305 . . . . . 6 class -1
1815, 16, 17cif 4119 . . . . 5 class if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)
1911, 12, 18cif 4119 . . . 4 class if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))
204, 7, 19cmpt 4762 . . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)))
212, 3, 20cmpt 4762 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))))
221, 21wceq 1523 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  29855
  Copyright terms: Public domain W3C validator