Metamath Proof Explorer


Theorem sgnsval

Description: The sign value. (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 sgnsval
|- ( ( R e. V /\ X e. B ) -> ( S ` X ) = if ( X = .0. , 0 , if ( .0. .< X , 1 , -u 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 5 adantr
 |-  ( ( R e. V /\ X e. B ) -> S = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )
7 eqeq1
 |-  ( x = X -> ( x = .0. <-> X = .0. ) )
8 breq2
 |-  ( x = X -> ( .0. .< x <-> .0. .< X ) )
9 8 ifbid
 |-  ( x = X -> if ( .0. .< x , 1 , -u 1 ) = if ( .0. .< X , 1 , -u 1 ) )
10 7 9 ifbieq2d
 |-  ( x = X -> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) = if ( X = .0. , 0 , if ( .0. .< X , 1 , -u 1 ) ) )
11 10 adantl
 |-  ( ( ( R e. V /\ X e. B ) /\ x = X ) -> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) = if ( X = .0. , 0 , if ( .0. .< X , 1 , -u 1 ) ) )
12 simpr
 |-  ( ( R e. V /\ X e. B ) -> X e. B )
13 c0ex
 |-  0 e. _V
14 13 a1i
 |-  ( ( ( R e. V /\ X e. B ) /\ X = .0. ) -> 0 e. _V )
15 1ex
 |-  1 e. _V
16 15 a1i
 |-  ( ( ( ( R e. V /\ X e. B ) /\ -. X = .0. ) /\ .0. .< X ) -> 1 e. _V )
17 negex
 |-  -u 1 e. _V
18 17 a1i
 |-  ( ( ( ( R e. V /\ X e. B ) /\ -. X = .0. ) /\ -. .0. .< X ) -> -u 1 e. _V )
19 16 18 ifclda
 |-  ( ( ( R e. V /\ X e. B ) /\ -. X = .0. ) -> if ( .0. .< X , 1 , -u 1 ) e. _V )
20 14 19 ifclda
 |-  ( ( R e. V /\ X e. B ) -> if ( X = .0. , 0 , if ( .0. .< X , 1 , -u 1 ) ) e. _V )
21 6 11 12 20 fvmptd
 |-  ( ( R e. V /\ X e. B ) -> ( S ` X ) = if ( X = .0. , 0 , if ( .0. .< X , 1 , -u 1 ) ) )