Theorem xrge0cmn

Description: The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	xrge0cmn	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
2	1	xrs1cmn	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\in \mathrm{CMnd}$$
3	1	xrge0subm	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{SubMnd}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$$
4		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
5	4	difexi	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}$$
6		difss	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$$
7		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
8	1 7	ressbas2	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\to {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)}$$
9	6 8	ax-mp	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)}$$
10	9	submss	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{SubMnd}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}$$
11	3 10	ax-mp	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}$$
12		ressabs	$$⊢\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\to \left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right){\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
13	5 11 12	mp2an	$$⊢\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right){\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
14	13	eqcomi	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]=\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right){\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
15	14	submmnd	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{SubMnd}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$$
16	3 15	ax-mp	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$$
17	14	subcmn	$$⊢\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\in \mathrm{CMnd}\wedge {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}\right)\to {ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$
18	2 16 17	mp2an	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$$