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	$⊢ R = ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})$
	Assertion	xrs1mnd	$⊢ R \in Mnd$

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	$⊢ R = ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})$
2		difss	$⊢ ℝ^{} ∖ \{−∞\} \subseteq ℝ^{}$
3		xrsbas	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
4	1 3	ressbas2	$⊢ ℝ^{} ∖ \{−∞\} \subseteq ℝ^{} \to ℝ^{*} ∖ \{−∞\} = {Base}_{R}$
5	2 4	mp1i	$⊢ ⊤ \to ℝ^{*} ∖ \{−∞\} = {Base}_{R}$
6		xrex	$⊢ ℝ^{*} \in V$
7	6	difexi	$⊢ ℝ^{*} ∖ \{−∞\} \in V$
8		xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
9	1 8	ressplusg	$⊢ ℝ^{*} ∖ \{−∞\} \in V \to +_{𝑒} = +_{R}$
10	7 9	mp1i	$⊢ ⊤ \to +_{𝑒} = +_{R}$
11		eldifsn	$⊢ x \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (x \in ℝ^{} \land x \neq −∞)$
12		eldifsn	$⊢ y \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (y \in ℝ^{} \land y \neq −∞)$
13		xaddcl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x +_{𝑒} y \in ℝ^{*}$
14	13	ad2ant2r	$⊢ ((x \in ℝ^{} \land x \neq −∞) \land (y \in ℝ^{} \land y \neq −∞)) \to x +_{𝑒} y \in ℝ^{*}$
15		xaddnemnf	$⊢ ((x \in ℝ^{} \land x \neq −∞) \land (y \in ℝ^{} \land y \neq −∞)) \to x +_{𝑒} y \neq −∞$
16		eldifsn	$⊢ x +_{𝑒} y \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (x +_{𝑒} y \in ℝ^{} \land x +_{𝑒} y \neq −∞)$
17	14 15 16	sylanbrc	$⊢ ((x \in ℝ^{} \land x \neq −∞) \land (y \in ℝ^{} \land y \neq −∞)) \to x +_{𝑒} y \in (ℝ^{*} ∖ \{−∞\})$
18	11 12 17	syl2anb	$⊢ (x \in (ℝ^{} ∖ \{−∞\}) \land y \in (ℝ^{} ∖ \{−∞\})) \to x +_{𝑒} y \in (ℝ^{*} ∖ \{−∞\})$
19	18	3adant1	$⊢ (⊤ \land x \in (ℝ^{} ∖ \{−∞\}) \land y \in (ℝ^{} ∖ \{−∞\})) \to x +_{𝑒} y \in (ℝ^{*} ∖ \{−∞\})$
20		eldifsn	$⊢ z \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (z \in ℝ^{} \land z \neq −∞)$
21		xaddass	$⊢ ((x \in ℝ^{} \land x \neq −∞) \land (y \in ℝ^{} \land y \neq −∞) \land (z \in ℝ^{*} \land z \neq −∞)) \to (x +_{𝑒} y) +_{𝑒} z = x +_{𝑒} (y +_{𝑒} z)$
22	11 12 20 21	syl3anb	$⊢ (x \in (ℝ^{} ∖ \{−∞\}) \land y \in (ℝ^{} ∖ \{−∞\}) \land z \in (ℝ^{*} ∖ \{−∞\})) \to (x +_{𝑒} y) +_{𝑒} z = x +_{𝑒} (y +_{𝑒} z)$
23	22	adantl	$⊢ (⊤ \land (x \in (ℝ^{} ∖ \{−∞\}) \land y \in (ℝ^{} ∖ \{−∞\}) \land z \in (ℝ^{*} ∖ \{−∞\}))) \to (x +_{𝑒} y) +_{𝑒} z = x +_{𝑒} (y +_{𝑒} z)$
24		0re	$⊢ 0 \in ℝ$
25		rexr	$⊢ 0 \in ℝ \to 0 \in ℝ^{*}$
26		renemnf	$⊢ 0 \in ℝ \to 0 \neq −∞$
27		eldifsn	$⊢ 0 \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (0 \in ℝ^{} \land 0 \neq −∞)$
28	25 26 27	sylanbrc	$⊢ 0 \in ℝ \to 0 \in (ℝ^{*} ∖ \{−∞\})$
29	24 28	mp1i	$⊢ ⊤ \to 0 \in (ℝ^{*} ∖ \{−∞\})$
30		eldifi	$⊢ x \in (ℝ^{} ∖ \{−∞\}) \to x \in ℝ^{}$
31	30	adantl	$⊢ (⊤ \land x \in (ℝ^{} ∖ \{−∞\})) \to x \in ℝ^{}$
32		xaddlid	$⊢ x \in ℝ^{*} \to 0 +_{𝑒} x = x$
33	31 32	syl	$⊢ (⊤ \land x \in (ℝ^{*} ∖ \{−∞\})) \to 0 +_{𝑒} x = x$
34	31	xaddridd	$⊢ (⊤ \land x \in (ℝ^{*} ∖ \{−∞\})) \to x +_{𝑒} 0 = x$
35	5 10 19 23 29 33 34	ismndd	$⊢ ⊤ \to R \in Mnd$
36	35	mptru	$⊢ R \in Mnd$

Metamath Proof Explorer

Theorem xrs1mnd

Proof