Metamath Proof Explorer


Theorem xrsmgm

Description: The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020)

Ref Expression
Assertion xrsmgm 𝑠*Mgm

Proof

Step Hyp Ref Expression
1 xaddcl x*y*x+𝑒y*
2 1 rgen2 x*y*x+𝑒y*
3 0xr 0*
4 xrsbas *=Base𝑠*
5 xrsadd +𝑒=+𝑠*
6 4 5 ismgmn0 0*𝑠*Mgmx*y*x+𝑒y*
7 3 6 ax-mp 𝑠*Mgmx*y*x+𝑒y*
8 2 7 mpbir 𝑠*Mgm