Theorem sgnsf

Description: The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	sgnsval.b	|- B = ( Base ` R )
	sgnsval.0	|- .0. = ( 0g ` R )
	sgnsval.l	|- .< = ( lt ` R )
	sgnsval.s	|- S = ( sgns ` R )
Assertion	sgnsf	|- ( R e. V -> S : B --> { -u 1 , 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		sgnsval.b	|- B = ( Base ` R )
2		sgnsval.0	|- .0. = ( 0g ` R )
3		sgnsval.l	|- .< = ( lt ` R )
4		sgnsval.s	|- S = ( sgns ` R )
5	1 2 3 4	sgnsv	|- ( R e. V -> S = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )
6		c0ex	|- 0 e. _V
7	6	tpid2	|- 0 e. { -u 1 , 0 , 1 }
8		1ex	|- 1 e. _V
9	8	tpid3	|- 1 e. { -u 1 , 0 , 1 }
10		negex	|- -u 1 e. _V
11	10	tpid1	|- -u 1 e. { -u 1 , 0 , 1 }
12	9 11	ifcli	|- if ( .0. .< x , 1 , -u 1 ) e. { -u 1 , 0 , 1 }
13	7 12	ifcli	|- if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) e. { -u 1 , 0 , 1 }
14	13	a1i	|- ( ( R e. V /\ x e. B ) -> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) e. { -u 1 , 0 , 1 } )
15	5 14	fmpt3d	|- ( R e. V -> S : B --> { -u 1 , 0 , 1 } )