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

Metamath Proof Explorer

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 [,] +∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( 0 [,] +∞ ) )
11 10 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +𝑒 𝑦 ) ∈ ( 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 ⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
21 1 20 ressplusg ⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → +𝑒 = ( +g ‘ 𝑅 ) )
22 19 21 ax-mp ⊢ +𝑒 = ( +g ‘ 𝑅 )
23 16 17 22 issubm ⊢ ( 𝑅 ∈ Mnd → ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 ) ↔ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +𝑒 𝑦 ) ∈ ( 0 [,] +∞ ) ) ) )
24 12 23 ax-mp ⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 ) ↔ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 +𝑒 𝑦 ) ∈ ( 0 [,] +∞ ) ) )
25 8 9 11 24 mpbir3an ⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ 𝑅 )