# Metamath Proof Explorer

## Theorem xrge0omnd

Description: The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018)

Ref Expression
Assertion xrge0omnd ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{oMnd}$

### Proof

Step Hyp Ref Expression
1 xrge0cmn ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$
2 cmnmnd ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}\to {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$
3 1 2 ax-mp ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$
4 ovex ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$
5 xrge0base ${⊢}\left[0,\mathrm{+\infty }\right]={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
6 xrge0le ${⊢}\le ={\le }_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
7 eliccxr ${⊢}{x}\in \left[0,\mathrm{+\infty }\right]\to {x}\in {ℝ}^{*}$
8 7 xrleidd ${⊢}{x}\in \left[0,\mathrm{+\infty }\right]\to {x}\le {x}$
9 eliccxr ${⊢}{y}\in \left[0,\mathrm{+\infty }\right]\to {y}\in {ℝ}^{*}$
10 xrletri3 ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x}={y}↔\left({x}\le {y}\wedge {y}\le {x}\right)\right)$
11 10 biimprd ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left(\left({x}\le {y}\wedge {y}\le {x}\right)\to {x}={y}\right)$
12 7 9 11 syl2an ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(\left({x}\le {y}\wedge {y}\le {x}\right)\to {x}={y}\right)$
13 eliccxr ${⊢}{z}\in \left[0,\mathrm{+\infty }\right]\to {z}\in {ℝ}^{*}$
14 xrletr ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\to \left(\left({x}\le {y}\wedge {y}\le {z}\right)\to {x}\le {z}\right)$
15 7 9 13 14 syl3an ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\wedge {z}\in \left[0,\mathrm{+\infty }\right]\right)\to \left(\left({x}\le {y}\wedge {y}\le {z}\right)\to {x}\le {z}\right)$
16 4 5 6 8 12 15 isposi ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Poset}$
17 xrletri ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x}\le {y}\vee {y}\le {x}\right)$
18 7 9 17 syl2an ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}\le {y}\vee {y}\le {x}\right)$
19 18 rgen2 ${⊢}\forall {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\vee {y}\le {x}\right)$
20 5 6 istos ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Toset}↔\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Poset}\wedge \forall {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\vee {y}\le {x}\right)\right)$
21 16 19 20 mpbir2an ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Toset}$
22 xleadd1a ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\wedge {x}\le {y}\right)\to {x}{+}_{𝑒}{z}\le {y}{+}_{𝑒}{z}$
23 22 ex ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\to \left({x}\le {y}\to {x}{+}_{𝑒}{z}\le {y}{+}_{𝑒}{z}\right)$
24 7 9 13 23 syl3an ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right]\wedge {y}\in \left[0,\mathrm{+\infty }\right]\wedge {z}\in \left[0,\mathrm{+\infty }\right]\right)\to \left({x}\le {y}\to {x}{+}_{𝑒}{z}\le {y}{+}_{𝑒}{z}\right)$
25 24 rgen3 ${⊢}\forall {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\to {x}{+}_{𝑒}{z}\le {y}{+}_{𝑒}{z}\right)$
26 xrge0plusg ${⊢}{+}_{𝑒}={+}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
27 5 26 6 isomnd ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{oMnd}↔\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}\wedge {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Toset}\wedge \forall {x}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\to {x}{+}_{𝑒}{z}\le {y}{+}_{𝑒}{z}\right)\right)$
28 3 21 25 27 mpbir3an ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{oMnd}$