Metamath Proof Explorer


Theorem xrsmcmn

Description: The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp .) (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsmcmn mulGrp𝑠*CMnd

Proof

Step Hyp Ref Expression
1 eqid mulGrp𝑠*=mulGrp𝑠*
2 xrsbas *=Base𝑠*
3 1 2 mgpbas *=BasemulGrp𝑠*
4 3 a1i *=BasemulGrp𝑠*
5 xrsmul 𝑒=𝑠*
6 1 5 mgpplusg 𝑒=+mulGrp𝑠*
7 6 a1i 𝑒=+mulGrp𝑠*
8 xmulcl x*y*x𝑒y*
9 8 3adant1 x*y*x𝑒y*
10 xmulass x*y*z*x𝑒y𝑒z=x𝑒y𝑒z
11 10 adantl x*y*z*x𝑒y𝑒z=x𝑒y𝑒z
12 1re 1
13 rexr 11*
14 12 13 mp1i 1*
15 xmulid2 x*1𝑒x=x
16 15 adantl x*1𝑒x=x
17 xmulid1 x*x𝑒1=x
18 17 adantl x*x𝑒1=x
19 4 7 9 11 14 16 18 ismndd mulGrp𝑠*Mnd
20 xmulcom x*y*x𝑒y=y𝑒x
21 20 3adant1 x*y*x𝑒y=y𝑒x
22 4 7 19 21 iscmnd mulGrp𝑠*CMnd
23 22 mptru mulGrp𝑠*CMnd