Theorem xrge0cmn

Description: The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
2	1	xrs1cmn	|- ( RR*s |`s ( RR* \ { -oo } ) ) e. CMnd
3	1	xrge0subm	|- ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) )
4		xrex	|- RR* e. _V
5	4	difexi	|- ( RR* \ { -oo } ) e. _V
6		difss	|- ( RR* \ { -oo } ) C_ RR*
7		xrsbas	|- RR* = ( Base ` RR*s )
8	1 7	ressbas2	|- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) ) )
9	6 8	ax-mp	|- ( RR* \ { -oo } ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) )
10	9	submss	|- ( ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) ) -> ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) )
11	3 10	ax-mp	|- ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
12		ressabs	|- ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) )
13	5 11 12	mp2an	|- ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
14	13	eqcomi	|- ( RR*s |`s ( 0 [,] +oo ) ) = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
15	14	submmnd	|- ( ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
16	3 15	ax-mp	|- ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
17	14	subcmn	|- ( ( ( RR*s |`s ( RR* \ { -oo } ) ) e. CMnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
18	2 16 17	mp2an	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd