Step |
Hyp |
Ref |
Expression |
0 |
|
cxrs |
|- RR*s |
1 |
|
cbs |
|- Base |
2 |
|
cnx |
|- ndx |
3 |
2 1
|
cfv |
|- ( Base ` ndx ) |
4 |
|
cxr |
|- RR* |
5 |
3 4
|
cop |
|- <. ( Base ` ndx ) , RR* >. |
6 |
|
cplusg |
|- +g |
7 |
2 6
|
cfv |
|- ( +g ` ndx ) |
8 |
|
cxad |
|- +e |
9 |
7 8
|
cop |
|- <. ( +g ` ndx ) , +e >. |
10 |
|
cmulr |
|- .r |
11 |
2 10
|
cfv |
|- ( .r ` ndx ) |
12 |
|
cxmu |
|- *e |
13 |
11 12
|
cop |
|- <. ( .r ` ndx ) , *e >. |
14 |
5 9 13
|
ctp |
|- { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } |
15 |
|
cts |
|- TopSet |
16 |
2 15
|
cfv |
|- ( TopSet ` ndx ) |
17 |
|
cordt |
|- ordTop |
18 |
|
cle |
|- <_ |
19 |
18 17
|
cfv |
|- ( ordTop ` <_ ) |
20 |
16 19
|
cop |
|- <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. |
21 |
|
cple |
|- le |
22 |
2 21
|
cfv |
|- ( le ` ndx ) |
23 |
22 18
|
cop |
|- <. ( le ` ndx ) , <_ >. |
24 |
|
cds |
|- dist |
25 |
2 24
|
cfv |
|- ( dist ` ndx ) |
26 |
|
vx |
|- x |
27 |
|
vy |
|- y |
28 |
26
|
cv |
|- x |
29 |
27
|
cv |
|- y |
30 |
28 29 18
|
wbr |
|- x <_ y |
31 |
28
|
cxne |
|- -e x |
32 |
29 31 8
|
co |
|- ( y +e -e x ) |
33 |
29
|
cxne |
|- -e y |
34 |
28 33 8
|
co |
|- ( x +e -e y ) |
35 |
30 32 34
|
cif |
|- if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) |
36 |
26 27 4 4 35
|
cmpo |
|- ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) |
37 |
25 36
|
cop |
|- <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. |
38 |
20 23 37
|
ctp |
|- { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } |
39 |
14 38
|
cun |
|- ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } ) |
40 |
0 39
|
wceq |
|- RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } ) |