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 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ oMnd

Proof

Step Hyp Ref Expression
1 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
2 cmnmnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
3 1 2 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
4 ovex ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ V
5 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
6 xrge0le ⊢ ≤ = ( le ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
7 eliccxr ⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ℝ* )
8 7 xrleidd ⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ≤ 𝑥 )
9 eliccxr ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → 𝑦 ∈ ℝ* )
10 xrletri3 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
11 10 biimprd ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
12 7 9 11 syl2an ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
13 eliccxr ⊢ ( 𝑧 ∈ ( 0 [,] +∞ ) → 𝑧 ∈ ℝ* )
14 xrletr ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
15 7 9 13 14 syl3an ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ∧ 𝑧 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
16 4 5 6 8 12 15 isposi ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Poset
17 xrletri ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
18 7 9 17 syl2an ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
19 18 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 )
20 5 6 istos ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Toset ↔ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Poset ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) )
21 16 19 20 mpbir2an ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Toset
22 xleadd1a ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 +𝑒 𝑧 ) ≤ ( 𝑦 +𝑒 𝑧 ) )
23 22 ex ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 → ( 𝑥 +𝑒 𝑧 ) ≤ ( 𝑦 +𝑒 𝑧 ) ) )
24 7 9 13 23 syl3an ⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ∧ 𝑧 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ≤ 𝑦 → ( 𝑥 +𝑒 𝑧 ) ≤ ( 𝑦 +𝑒 𝑧 ) ) )
25 24 rgen3 ⊢ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ∀ 𝑧 ∈ ( 0 [,] +∞ ) ( 𝑥 ≤ 𝑦 → ( 𝑥 +𝑒 𝑧 ) ≤ ( 𝑦 +𝑒 𝑧 ) )
26 xrge0plusg ⊢ +𝑒 = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
27 5 26 6 isomnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ oMnd ↔ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Toset ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ∀ 𝑧 ∈ ( 0 [,] +∞ ) ( 𝑥 ≤ 𝑦 → ( 𝑥 +𝑒 𝑧 ) ≤ ( 𝑦 +𝑒 𝑧 ) ) ) )
28 3 21 25 27 mpbir3an ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ oMnd