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