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

Metamath Proof Explorer

Theorem xrs1cmn

Description: The extended real numbers restricted to RR* \ { -oo } form a commutative monoid. They are not a group because 1 + +oo = 2 + +oo even though 1 =/= 2 . (Contributed by Mario Carneiro, 27-Nov-2014)

Ref Expression
Hypothesis xrs1mnd.1 ⊢ R = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
Assertion xrs1cmn ⊢ R ∈ CMnd

Proof

Step Hyp Ref Expression
1 xrs1mnd.1 ⊢ R = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
2 1 xrs1mnd ⊢ R ∈ Mnd
3 eldifi ⊢ x ∈ ℝ * ∖ −∞ → x ∈ ℝ *
4 eldifi ⊢ y ∈ ℝ * ∖ −∞ → y ∈ ℝ *
5 xaddcom ⊢ x ∈ ℝ * ∧ y ∈ ℝ * → x + 𝑒 y = y + 𝑒 x
6 3 4 5 syl2an ⊢ x ∈ ℝ * ∖ −∞ ∧ y ∈ ℝ * ∖ −∞ → x + 𝑒 y = y + 𝑒 x
7 6 rgen2 ⊢ ∀ x ∈ ℝ * ∖ −∞ ∀ y ∈ ℝ * ∖ −∞ x + 𝑒 y = y + 𝑒 x
8 difss ⊢ ℝ * ∖ −∞ ⊆ ℝ *
9 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
10 1 9 ressbas2 ⊢ ℝ * ∖ −∞ ⊆ ℝ * → ℝ * ∖ −∞ = Base R
11 8 10 ax-mp ⊢ ℝ * ∖ −∞ = Base R
12 xrex ⊢ ℝ * ∈ V
13 12 difexi ⊢ ℝ * ∖ −∞ ∈ V
14 xrsadd ⊢ + 𝑒 = + ℝ 𝑠 *
15 1 14 ressplusg ⊢ ℝ * ∖ −∞ ∈ V → + 𝑒 = + R
16 13 15 ax-mp ⊢ + 𝑒 = + R
17 11 16 iscmn ⊢ R ∈ CMnd ↔ R ∈ Mnd ∧ ∀ x ∈ ℝ * ∖ −∞ ∀ y ∈ ℝ * ∖ −∞ x + 𝑒 y = y + 𝑒 x
18 2 7 17 mpbir2an ⊢ R ∈ CMnd