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 = ( RRs \|`s ( RR \ { -oo } ) )
	Assertion	xrge0subm	\|- ( 0 [,] +oo ) e. ( SubMnd ` R )

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	\|- R = ( RRs \|`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 )

Metamath Proof Explorer

Theorem xrge0subm

Proof