Description: The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xrsadd | |- +e = ( +g ` RR*s ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xaddf | |- +e : ( RR* X. RR* ) --> RR* |
|
2 | xrex | |- RR* e. _V |
|
3 | 2 2 | xpex | |- ( RR* X. RR* ) e. _V |
4 | fex2 | |- ( ( +e : ( RR* X. RR* ) --> RR* /\ ( RR* X. RR* ) e. _V /\ RR* e. _V ) -> +e e. _V ) |
|
5 | 1 3 2 4 | mp3an | |- +e e. _V |
6 | df-xrs | |- 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 ) ) ) >. } ) |
|
7 | 6 | odrngplusg | |- ( +e e. _V -> +e = ( +g ` RR*s ) ) |
8 | 5 7 | ax-mp | |- +e = ( +g ` RR*s ) |