Definition df-sgns 31426

Description: Signum function for a structure. See also df-sgn 14798 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

Step	Hyp	Ref	Expression
1		csgns 31425	. 2 class sgns
2		vr	. . 3 setvar 𝑟
3		cvv 3432	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1538	. . . . 5 class 𝑟
6		cbs 16912	. . . . 5 class Base
7	5, 6	cfv 6433	. . . 4 class (Base‘𝑟)
8	4	cv 1538	. . . . . 6 class 𝑥
9		c0g 17150	. . . . . . 7 class 0g
10	5, 9	cfv 6433	. . . . . 6 class (0g‘𝑟)
11	8, 10	wceq 1539	. . . . 5 wff 𝑥 = (0g‘𝑟)
12		cc0 10871	. . . . 5 class 0
13		cplt 18026	. . . . . . . 8 class lt
14	5, 13	cfv 6433	. . . . . . 7 class (lt‘𝑟)
15	10, 8, 14	wbr 5074	. . . . . 6 wff (0g‘𝑟)(lt‘𝑟)𝑥
16		c1 10872	. . . . . 6 class 1
17	16	cneg 11206	. . . . . 6 class -1
18	15, 16, 17	cif 4459	. . . . 5 class if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)
19	11, 12, 18	cif 4459	. . . 4 class if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))
20	4, 7, 19	cmpt 5157	. . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))
21	2, 3, 20	cmpt 5157	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))
22	1, 21	wceq 1539	1 wff sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))

This definition is referenced by:  sgnsv  31427