Definition df-sgns 33222

Description: Signum function for a structure. See also df-sgn 15014 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 33221	. 2 class sgns
2		vr	. . 3 setvar 𝑟
3		cvv 3441	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1541	. . . . 5 class 𝑟
6		cbs 17140	. . . . 5 class Base
7	5, 6	cfv 6493	. . . 4 class (Base‘𝑟)
8	4	cv 1541	. . . . . 6 class 𝑥
9		c0g 17363	. . . . . . 7 class 0g
10	5, 9	cfv 6493	. . . . . 6 class (0g‘𝑟)
11	8, 10	wceq 1542	. . . . 5 wff 𝑥 = (0g‘𝑟)
12		cc0 11030	. . . . 5 class 0
13		cplt 18235	. . . . . . . 8 class lt
14	5, 13	cfv 6493	. . . . . . 7 class (lt‘𝑟)
15	10, 8, 14	wbr 5099	. . . . . 6 wff (0g‘𝑟)(lt‘𝑟)𝑥
16		c1 11031	. . . . . 6 class 1
17	16	cneg 11369	. . . . . 6 class -1
18	15, 16, 17	cif 4480	. . . . 5 class if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)
19	11, 12, 18	cif 4480	. . . 4 class if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))
20	4, 7, 19	cmpt 5180	. . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))
21	2, 3, 20	cmpt 5180	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))
22	1, 21	wceq 1542	1 wff sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))

This definition is referenced by:  sgnsv  33223