Definition df-sgns 29057

Description: Signum function for a structure. See also df-sgn 13675 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 29056	. 2 class sgns
2		vr	. . 3 setvar 𝑟
3		cvv 3173	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1474	. . . . 5 class 𝑟
6		cbs 15695	. . . . 5 class Base
7	5, 6	cfv 5804	. . . 4 class (Base‘𝑟)
8	4	cv 1474	. . . . . 6 class 𝑥
9		c0g 15923	. . . . . . 7 class 0g
10	5, 9	cfv 5804	. . . . . 6 class (0g‘𝑟)
11	8, 10	wceq 1475	. . . . 5 wff 𝑥 = (0g‘𝑟)
12		cc0 9815	. . . . 5 class 0
13		cplt 16764	. . . . . . . 8 class lt
14	5, 13	cfv 5804	. . . . . . 7 class (lt‘𝑟)
15	10, 8, 14	wbr 4583	. . . . . 6 wff (0g‘𝑟)(lt‘𝑟)𝑥
16		c1 9816	. . . . . 6 class 1
17	16	cneg 10146	. . . . . 6 class -1
18	15, 16, 17	cif 4036	. . . . 5 class if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)
19	11, 12, 18	cif 4036	. . . 4 class if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))
20	4, 7, 19	cmpt 4643	. . 3 class (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))
21	2, 3, 20	cmpt 4643	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))
22	1, 21	wceq 1475	1 wff sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))

This definition is referenced by:  sgnsv  29058