Metamath Proof Explorer


Theorem xrsadd

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 )

Proof

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 )