Theorem xrs1mnd

Description: The extended real numbers, restricted to RR* \ { -oo } , form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp . (Contributed by Mario Carneiro, 27-Nov-2014)

	Ref	Expression
Hypothesis	xrs1mnd.1	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
Assertion	xrs1mnd	⊢ 𝑅 ∈ Mnd

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
3		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
4	1 3	ressbas2	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 ) )
5	2 4	mp1i	⊢ ( ⊤ → ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 ) )
6		xrex	⊢ ℝ* ∈ V
7	6	difexi	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
8		xrsadd	⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
9	1 8	ressplusg	⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → +𝑒 = ( +g ‘ 𝑅 ) )
10	7 9	mp1i	⊢ ( ⊤ → +𝑒 = ( +g ‘ 𝑅 ) )
11		eldifsn	⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
12		eldifsn	⊢ ( 𝑦 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞ ) )
13		xaddcl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
14	13	ad2ant2r	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
15		xaddnemnf	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ≠ -∞ )
16		eldifsn	⊢ ( ( 𝑥 +𝑒 𝑦 ) ∈ ( ℝ* ∖ { -∞ } ) ↔ ( ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* ∧ ( 𝑥 +𝑒 𝑦 ) ≠ -∞ ) )
17	14 15 16	sylanbrc	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞ ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( ℝ* ∖ { -∞ } ) )
18	11 12 17	syl2anb	⊢ ( ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑦 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( ℝ* ∖ { -∞ } ) )
19	18	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑦 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ( ℝ* ∖ { -∞ } ) )
20		eldifsn	⊢ ( 𝑧 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) )
21		xaddass	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞ ) ∧ ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) ) → ( ( 𝑥 +𝑒 𝑦 ) +𝑒 𝑧 ) = ( 𝑥 +𝑒 ( 𝑦 +𝑒 𝑧 ) ) )
22	11 12 20 21	syl3anb	⊢ ( ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑦 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑧 ∈ ( ℝ* ∖ { -∞ } ) ) → ( ( 𝑥 +𝑒 𝑦 ) +𝑒 𝑧 ) = ( 𝑥 +𝑒 ( 𝑦 +𝑒 𝑧 ) ) )
23	22	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑦 ∈ ( ℝ* ∖ { -∞ } ) ∧ 𝑧 ∈ ( ℝ* ∖ { -∞ } ) ) ) → ( ( 𝑥 +𝑒 𝑦 ) +𝑒 𝑧 ) = ( 𝑥 +𝑒 ( 𝑦 +𝑒 𝑧 ) ) )
24		0re	⊢ 0 ∈ ℝ
25		rexr	⊢ ( 0 ∈ ℝ → 0 ∈ ℝ* )
26		renemnf	⊢ ( 0 ∈ ℝ → 0 ≠ -∞ )
27		eldifsn	⊢ ( 0 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 0 ∈ ℝ* ∧ 0 ≠ -∞ ) )
28	25 26 27	sylanbrc	⊢ ( 0 ∈ ℝ → 0 ∈ ( ℝ* ∖ { -∞ } ) )
29	24 28	mp1i	⊢ ( ⊤ → 0 ∈ ( ℝ* ∖ { -∞ } ) )
30		eldifi	⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) → 𝑥 ∈ ℝ* )
31	30	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → 𝑥 ∈ ℝ* )
32		xaddid2	⊢ ( 𝑥 ∈ ℝ* → ( 0 +𝑒 𝑥 ) = 𝑥 )
33	31 32	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 0 +𝑒 𝑥 ) = 𝑥 )
34	31	xaddid1d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑥 +𝑒 0 ) = 𝑥 )
35	5 10 19 23 29 33 34	ismndd	⊢ ( ⊤ → 𝑅 ∈ Mnd )
36	35	mptru	⊢ 𝑅 ∈ Mnd