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	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
Assertion	xrge0subm	⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2		simpl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
3		ge0nemnf	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ≠ -∞ )
4	2 3	jca	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
5		elxrge0	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) )
6		eldifsn	⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
7	4 5 6	3imtr4i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ( ℝ* ∖ { -∞ } ) )
8	7	ssriv	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
9		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
10		ge0xaddcl	⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 +e 𝑦 ) ∈ ( 0 [,] +∞ ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +e 𝑦 ) ∈ ( 0 [,] +∞ )
12	1	xrs1mnd	⊢ 𝑅 ∈ Mnd
13		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
14		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
15	1 14	ressbas2	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 ) )
16	13 15	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 )
17	1	xrs10	⊢ 0 = ( 0g ‘ 𝑅 )
18		xrex	⊢ ℝ* ∈ V
19	18	difexi	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
20		xrsadd	⊢ +e = ( +g ‘ ℝ*𝑠 )
21	1 20	ressplusg	⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → +e = ( +g ‘ 𝑅 ) )
22	19 21	ax-mp	⊢ +e = ( +g ‘ 𝑅 )
23	16 17 22	issubm	⊢ ( 𝑅 ∈ Mnd → ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 ) ↔ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +e 𝑦 ) ∈ ( 0 [,] +∞ ) ) ) )
24	12 23	ax-mp	⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 ) ↔ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +e 𝑦 ) ∈ ( 0 [,] +∞ ) ) )
25	8 9 11 24	mpbir3an	⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 )