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	$$⊢R={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
Assertion	xrs1cmn	$$⊢R\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	$$⊢R={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
2	1	xrs1mnd	$$⊢R\in \mathrm{Mnd}$$
3		eldifi	$$⊢x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\to x\in {ℝ}^{*}$$
4		eldifi	$$⊢y\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\to y\in {ℝ}^{*}$$
5		xaddcom	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{+}_{𝑒}y=y{+}_{𝑒}x$$
6	3 4 5	syl2an	$$⊢\left(x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\wedge y\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to x{+}_{𝑒}y=y{+}_{𝑒}x$$
7	6	rgen2	$$⊢\forall x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\forall y\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)x{+}_{𝑒}y=y{+}_{𝑒}x$$
8		difss	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$$
9		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
10	1 9	ressbas2	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\to {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_R$$
11	8 10	ax-mp	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_R$$
12		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
13	12	difexi	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}$$
14		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
15	1 14	ressplusg	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}\to {+}_{𝑒}={+}_R$$
16	13 15	ax-mp	$$⊢{+}_{𝑒}={+}_R$$
17	11 16	iscmn	$$⊢R\in \mathrm{CMnd}\leftrightarrow \left(R\in \mathrm{Mnd}\wedge \forall x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\forall y\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)x{+}_{𝑒}y=y{+}_{𝑒}x\right)$$
18	2 7 17	mpbir2an	$$⊢R\in \mathrm{CMnd}$$