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 ) ) ) |