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

Metamath Proof Explorer

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