Definition df-sgns

Description: Signum function for a structure. See also df-sgn for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018)

	Ref	Expression
Assertion	df-sgns	⊢ sgns = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgns	⊢ sgns
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7	3	cv	⊢ 𝑥
8		c0g	⊢ 0g
9	5 8	cfv	⊢ ( 0g ‘ 𝑟 )
10	7 9	wceq	⊢ 𝑥 = ( 0g ‘ 𝑟 )
11		cc0	⊢ 0
12		cplt	⊢ lt
13	5 12	cfv	⊢ ( lt ‘ 𝑟 )
14	9 7 13	wbr	⊢ ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥
15		c1	⊢ 1
16	15	cneg	⊢ - 1
17	14 15 16	cif	⊢ if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 )
18	10 11 17	cif	⊢ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) )
19	3 6 18	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) )
20	1 2 19	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) ) )
21	0 20	wceq	⊢ sgns = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) ) )