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 ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd

Proof

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