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 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2 1 xrs1cmn ⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd
3 1 xrge0subm ⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
4 xrex ⊢ ℝ* ∈ V
5 4 difexi ⊢ ( ℝ* ∖ { -∞ } ) ∈ V
6 difss ⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
7 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
8 1 7 ressbas2 ⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) )
9 6 8 ax-mp ⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
10 9 submss ⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) )
11 3 10 ax-mp ⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
12 ressabs ⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
13 5 11 12 mp2an ⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
14 13 eqcomi ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
15 14 submmnd ⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
16 3 15 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
17 14 subcmn ⊢ ( ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
18 2 16 17 mp2an ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd