Theorem xrge0subm

Description: The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypothesis	xrs1mnd.1	|- R = ( RR*s |`s ( RR* \ { -oo } ) )
Assertion	xrge0subm	|- ( 0 [,] +oo ) e. ( SubMnd ` R )

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	|- R = ( RR*s |`s ( RR* \ { -oo } ) )
2		simpl	|- ( ( x e. RR* /\ 0 <_ x ) -> x e. RR* )
3		ge0nemnf	|- ( ( x e. RR* /\ 0 <_ x ) -> x =/= -oo )
4	2 3	jca	|- ( ( x e. RR* /\ 0 <_ x ) -> ( x e. RR* /\ x =/= -oo ) )
5		elxrge0	|- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
6		eldifsn	|- ( x e. ( RR* \ { -oo } ) <-> ( x e. RR* /\ x =/= -oo ) )
7	4 5 6	3imtr4i	|- ( x e. ( 0 [,] +oo ) -> x e. ( RR* \ { -oo } ) )
8	7	ssriv	|- ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
9		0e0iccpnf	|- 0 e. ( 0 [,] +oo )
10		ge0xaddcl	|- ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x +e y ) e. ( 0 [,] +oo ) )
11	10	rgen2	|- A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( x +e y ) e. ( 0 [,] +oo )
12	1	xrs1mnd	|- R e. Mnd
13		difss	|- ( RR* \ { -oo } ) C_ RR*
14		xrsbas	|- RR* = ( Base ` RR*s )
15	1 14	ressbas2	|- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` R ) )
16	13 15	ax-mp	|- ( RR* \ { -oo } ) = ( Base ` R )
17	1	xrs10	|- 0 = ( 0g ` R )
18		xrex	|- RR* e. _V
19	18	difexi	|- ( RR* \ { -oo } ) e. _V
20		xrsadd	|- +e = ( +g ` RR*s )
21	1 20	ressplusg	|- ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` R ) )
22	19 21	ax-mp	|- +e = ( +g ` R )
23	16 17 22	issubm	|- ( R e. Mnd -> ( ( 0 [,] +oo ) e. ( SubMnd ` R ) <-> ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) /\ 0 e. ( 0 [,] +oo ) /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( x +e y ) e. ( 0 [,] +oo ) ) ) )
24	12 23	ax-mp	|- ( ( 0 [,] +oo ) e. ( SubMnd ` R ) <-> ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) /\ 0 e. ( 0 [,] +oo ) /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( x +e y ) e. ( 0 [,] +oo ) ) )
25	8 9 11 24	mpbir3an	|- ( 0 [,] +oo ) e. ( SubMnd ` R )