Definition df-sgns 30473

Description: Signum function for a structure. See also df-sgn 14307 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 30472	. 2 class sgns
2		vr	. . 3 setvar 𝑟
3		cvv 3415	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1506	. . . . 5 class 𝑟
6		cbs 16339	. . . . 5 class Base
7	5, 6	cfv 6188	. . . 4 class (Base‘𝑟)
8	4	cv 1506	. . . . . 6 class 𝑥
9		c0g 16569	. . . . . . 7 class 0g
10	5, 9	cfv 6188	. . . . . 6 class (0g‘𝑟)
11	8, 10	wceq 1507	. . . . 5 wff 𝑥 = (0g‘𝑟)
12		cc0 10335	. . . . 5 class 0
13		cplt 17409	. . . . . . . 8 class lt
14	5, 13	cfv 6188	. . . . . . 7 class (lt‘𝑟)
15	10, 8, 14	wbr 4929	. . . . . 6 wff (0g‘𝑟)(lt‘𝑟)𝑥
16		c1 10336	. . . . . 6 class 1
17	16	cneg 10671	. . . . . 6 class -1
18	15, 16, 17	cif 4350	. . . . 5 class if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)
19	11, 12, 18	cif 4350	. . . 4 class if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))
20	4, 7, 19	cmpt 5008	. . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))
21	2, 3, 20	cmpt 5008	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))
22	1, 21	wceq 1507	1 wff sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))

This definition is referenced by:  sgnsv  30474