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 ⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
Assertion xrs1cmn 𝑅 ∈ CMnd

Proof

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