This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrge0plusg

Description: The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017)

Ref Expression
Assertion xrge0plusg ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞

Proof

Step Hyp Ref Expression
1 ovex ⊢ 0 +∞ ∈ V
2 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
3 xrsadd ⊢ + 𝑒 = + ℝ 𝑠 *
4 2 3 ressplusg ⊢ 0 +∞ ∈ V → + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
5 1 4 ax-mp ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞