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		xaddlid	⊢ ( 𝑥 ∈ ℝ^* → ( 0 +_𝑒 𝑥 ) = 𝑥 )
33	31 32	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ^* ∖ { -∞ } ) ) → ( 0 +_𝑒 𝑥 ) = 𝑥 )
34	31	xaddridd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ^* ∖ { -∞ } ) ) → ( 𝑥 +_𝑒 0 ) = 𝑥 )
35	5 10 19 23 29 33 34	ismndd	⊢ ( ⊤ → 𝑅 ∈ Mnd )
36	35	mptru	⊢ 𝑅 ∈ Mnd

Metamath Proof Explorer

Theorem xrs1mnd

Proof