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

Metamath Proof Explorer

Theorem xrsmul

Description: The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsmul ⊢ ⋅ 𝑒 = ⋅ ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 xmulf ⊢ ⋅ 𝑒 : ℝ * × ℝ * ⟶ ℝ *
2 xrex ⊢ ℝ * ∈ V
3 2 2 xpex ⊢ ℝ * × ℝ * ∈ V
4 fex2 ⊢ ⋅ 𝑒 : ℝ * × ℝ * ⟶ ℝ * ∧ ℝ * × ℝ * ∈ V ∧ ℝ * ∈ V → ⋅ 𝑒 ∈ V
5 1 3 2 4 mp3an ⊢ ⋅ 𝑒 ∈ V
6 df-xrs ⊢ ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
7 6 odrngmulr ⊢ ⋅ 𝑒 ∈ V → ⋅ 𝑒 = ⋅ ℝ 𝑠 *
8 5 7 ax-mp ⊢ ⋅ 𝑒 = ⋅ ℝ 𝑠 *