Metamath Proof Explorer

Theorem sgnsv

Description: The sign mapping. (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 sgnsv 
|- ( R e. V -> S = ( x e. B |-> 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 elex 
 |-  ( R e. V -> R e. _V )
6 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
7 6 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
8 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
9 8 2 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
10 9 adantr 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> ( 0g ` r ) = .0. )
11 10 eqeq2d 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> ( x = ( 0g ` r ) <-> x = .0. ) )
12 fveq2 
 |-  ( r = R -> ( lt ` r ) = ( lt ` R ) )
13 12 3 eqtr4di 
 |-  ( r = R -> ( lt ` r ) = .< )
14 13 adantr 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> ( lt ` r ) = .< )
15 eqidd 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> x = x )
16 10 14 15 breq123d 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> ( ( 0g ` r ) ( lt ` r ) x <-> .0. .< x ) )
17 16 ifbid 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) = if ( .0. .< x , 1 , -u 1 ) )
18 11 17 ifbieq2d 
 |-  ( ( r = R /\ x e. ( Base ` r ) ) -> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) = if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) )
19 7 18 mpteq12dva 
 |-  ( r = R -> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )
20 df-sgns 
 |-  sgns = ( r e. _V |-> ( x e. ( Base ` r ) |-> if ( x = ( 0g ` r ) , 0 , if ( ( 0g ` r ) ( lt ` r ) x , 1 , -u 1 ) ) ) )
21 19 20 1 mptfvmpt 
 |-  ( R e. _V -> ( sgns ` R ) = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )
22 5 21 syl 
 |-  ( R e. V -> ( sgns ` R ) = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )
23 4 22 syl5eq 
 |-  ( R e. V -> S = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )