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