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 𝑒 = 𝑠 *