This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrs1cmn

Description: The extended real numbers restricted to RR* \ { -oo } form a commutative monoid. They are not a group because 1 + +oo = 2 + +oo even though 1 =/= 2 . (Contributed by Mario Carneiro, 27-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 xrs1mnd.1 
 |-  R = ( RR*s |`s ( RR* \ { -oo } ) )
2 1 xrs1mnd 
 |-  R e. Mnd
3 eldifi 
 |-  ( x e. ( RR* \ { -oo } ) -> x e. RR* )
4 eldifi 
 |-  ( y e. ( RR* \ { -oo } ) -> y e. RR* )
5 xaddcom 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x +e y ) = ( y +e x ) )
6 3 4 5 syl2an 
 |-  ( ( x e. ( RR* \ { -oo } ) /\ y e. ( RR* \ { -oo } ) ) -> ( x +e y ) = ( y +e x ) )
7 6 rgen2 
 |-  A. x e. ( RR* \ { -oo } ) A. y e. ( RR* \ { -oo } ) ( x +e y ) = ( y +e x )
8 difss 
 |-  ( RR* \ { -oo } ) C_ RR*
9 xrsbas 
 |-  RR* = ( Base ` RR*s )
10 1 9 ressbas2 
 |-  ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` R ) )
11 8 10 ax-mp 
 |-  ( RR* \ { -oo } ) = ( Base ` R )
12 xrex 
 |-  RR* e. _V
13 12 difexi 
 |-  ( RR* \ { -oo } ) e. _V
14 xrsadd 
 |-  +e = ( +g ` RR*s )
15 1 14 ressplusg 
 |-  ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` R ) )
16 13 15 ax-mp 
 |-  +e = ( +g ` R )
17 11 16 iscmn 
 |-  ( R e. CMnd <-> ( R e. Mnd /\ A. x e. ( RR* \ { -oo } ) A. y e. ( RR* \ { -oo } ) ( x +e y ) = ( y +e x ) ) )
18 2 7 17 mpbir2an 
 |-  R e. CMnd