| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xrs1mnd.1 |
|- R = ( RR*s |`s ( RR* \ { -oo } ) ) |
| 2 |
|
difss |
|- ( RR* \ { -oo } ) C_ RR* |
| 3 |
|
xrsbas |
|- RR* = ( Base ` RR*s ) |
| 4 |
1 3
|
ressbas2 |
|- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` R ) ) |
| 5 |
2 4
|
ax-mp |
|- ( RR* \ { -oo } ) = ( Base ` R ) |
| 6 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
| 7 |
|
xrex |
|- RR* e. _V |
| 8 |
7
|
difexi |
|- ( RR* \ { -oo } ) e. _V |
| 9 |
|
xrsadd |
|- +e = ( +g ` RR*s ) |
| 10 |
1 9
|
ressplusg |
|- ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` R ) ) |
| 11 |
8 10
|
ax-mp |
|- +e = ( +g ` R ) |
| 12 |
|
0re |
|- 0 e. RR |
| 13 |
|
rexr |
|- ( 0 e. RR -> 0 e. RR* ) |
| 14 |
|
renemnf |
|- ( 0 e. RR -> 0 =/= -oo ) |
| 15 |
|
eldifsn |
|- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) ) |
| 16 |
13 14 15
|
sylanbrc |
|- ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) ) |
| 17 |
12 16
|
mp1i |
|- ( T. -> 0 e. ( RR* \ { -oo } ) ) |
| 18 |
|
eldifi |
|- ( x e. ( RR* \ { -oo } ) -> x e. RR* ) |
| 19 |
18
|
adantl |
|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> x e. RR* ) |
| 20 |
|
xaddlid |
|- ( x e. RR* -> ( 0 +e x ) = x ) |
| 21 |
19 20
|
syl |
|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( 0 +e x ) = x ) |
| 22 |
19
|
xaddridd |
|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( x +e 0 ) = x ) |
| 23 |
5 6 11 17 21 22
|
ismgmid2 |
|- ( T. -> 0 = ( 0g ` R ) ) |
| 24 |
23
|
mptru |
|- 0 = ( 0g ` R ) |