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 29503
Description: Signum function for a structure. See also df-sgn 13756 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 29502 . 2 class sgns
2 vr . . 3 setvar 𝑟
3 cvv 3191 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1479 . . . . 5 class 𝑟
6 cbs 15776 . . . . 5 class Base
75, 6cfv 5850 . . . 4 class (Base‘𝑟)
84cv 1479 . . . . . 6 class 𝑥
9 c0g 16016 . . . . . . 7 class 0g
105, 9cfv 5850 . . . . . 6 class (0g𝑟)
118, 10wceq 1480 . . . . 5 wff 𝑥 = (0g𝑟)
12 cc0 9881 . . . . 5 class 0
13 cplt 16857 . . . . . . . 8 class lt
145, 13cfv 5850 . . . . . . 7 class (lt‘𝑟)
1510, 8, 14wbr 4618 . . . . . 6 wff (0g𝑟)(lt‘𝑟)𝑥
16 c1 9882 . . . . . 6 class 1
1716cneg 10212 . . . . . 6 class -1
1815, 16, 17cif 4063 . . . . 5 class if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)
1911, 12, 18cif 4063 . . . 4 class if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))
204, 7, 19cmpt 4678 . . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1)))
212, 3, 20cmpt 4678 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g𝑟), 0, if((0g𝑟)(lt‘𝑟)𝑥, 1, -1))))
221, 21wceq 1480 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  29504
  Copyright terms: Public domain W3C validator