Metamath Proof Explorer

Theorem xrs1mnd

Description: The extended real numbers, restricted to RR* \ { -oo } , form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp . (Contributed by Mario Carneiro, 27-Nov-2014)

Ref Expression
Hypothesis xrs1mnd.1 
|- R = ( RR*s |`s ( RR* \ { -oo } ) )
Assertion xrs1mnd 
|- R e. Mnd

Proof

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 mp1i 
 |-  ( T. -> ( RR* \ { -oo } ) = ( Base ` R ) )
6 xrex 
 |-  RR* e. _V
7 6 difexi 
 |-  ( RR* \ { -oo } ) e. _V
8 xrsadd 
 |-  +e = ( +g ` RR*s )
9 1 8 ressplusg 
 |-  ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` R ) )
10 7 9 mp1i 
 |-  ( T. -> +e = ( +g ` R ) )
11 eldifsn 
 |-  ( x e. ( RR* \ { -oo } ) <-> ( x e. RR* /\ x =/= -oo ) )
12 eldifsn 
 |-  ( y e. ( RR* \ { -oo } ) <-> ( y e. RR* /\ y =/= -oo ) )
13 xaddcl 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x +e y ) e. RR* )
14 13 ad2ant2r 
 |-  ( ( ( x e. RR* /\ x =/= -oo ) /\ ( y e. RR* /\ y =/= -oo ) ) -> ( x +e y ) e. RR* )
15 xaddnemnf 
 |-  ( ( ( x e. RR* /\ x =/= -oo ) /\ ( y e. RR* /\ y =/= -oo ) ) -> ( x +e y ) =/= -oo )
16 eldifsn 
 |-  ( ( x +e y ) e. ( RR* \ { -oo } ) <-> ( ( x +e y ) e. RR* /\ ( x +e y ) =/= -oo ) )
17 14 15 16 sylanbrc 
 |-  ( ( ( x e. RR* /\ x =/= -oo ) /\ ( y e. RR* /\ y =/= -oo ) ) -> ( x +e y ) e. ( RR* \ { -oo } ) )
18 11 12 17 syl2anb 
 |-  ( ( x e. ( RR* \ { -oo } ) /\ y e. ( RR* \ { -oo } ) ) -> ( x +e y ) e. ( RR* \ { -oo } ) )
19 18 3adant1 
 |-  ( ( T. /\ x e. ( RR* \ { -oo } ) /\ y e. ( RR* \ { -oo } ) ) -> ( x +e y ) e. ( RR* \ { -oo } ) )
20 eldifsn 
 |-  ( z e. ( RR* \ { -oo } ) <-> ( z e. RR* /\ z =/= -oo ) )
21 xaddass 
 |-  ( ( ( x e. RR* /\ x =/= -oo ) /\ ( y e. RR* /\ y =/= -oo ) /\ ( z e. RR* /\ z =/= -oo ) ) -> ( ( x +e y ) +e z ) = ( x +e ( y +e z ) ) )
22 11 12 20 21 syl3anb 
 |-  ( ( x e. ( RR* \ { -oo } ) /\ y e. ( RR* \ { -oo } ) /\ z e. ( RR* \ { -oo } ) ) -> ( ( x +e y ) +e z ) = ( x +e ( y +e z ) ) )
23 22 adantl 
 |-  ( ( T. /\ ( x e. ( RR* \ { -oo } ) /\ y e. ( RR* \ { -oo } ) /\ z e. ( RR* \ { -oo } ) ) ) -> ( ( x +e y ) +e z ) = ( x +e ( y +e z ) ) )
24 0re 
 |-  0 e. RR
25 rexr 
 |-  ( 0 e. RR -> 0 e. RR* )
26 renemnf 
 |-  ( 0 e. RR -> 0 =/= -oo )
27 eldifsn 
 |-  ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
28 25 26 27 sylanbrc 
 |-  ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
29 24 28 mp1i 
 |-  ( T. -> 0 e. ( RR* \ { -oo } ) )
30 eldifi 
 |-  ( x e. ( RR* \ { -oo } ) -> x e. RR* )
31 30 adantl 
 |-  ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> x e. RR* )
32 xaddlid 
 |-  ( x e. RR* -> ( 0 +e x ) = x )
33 31 32 syl 
 |-  ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( 0 +e x ) = x )
34 31 xaddridd 
 |-  ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( x +e 0 ) = x )
35 5 10 19 23 29 33 34 ismndd 
 |-  ( T. -> R e. Mnd )
36 35 mptru 
 |-  R e. Mnd