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

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 ` RR*s ) e. CMnd

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( mulGrp ` RR*s ) = ( mulGrp ` RR*s )
2 xrsbas 
 |-  RR* = ( Base ` RR*s )
3 1 2 mgpbas 
 |-  RR* = ( Base ` ( mulGrp ` RR*s ) )
4 3 a1i 
 |-  ( T. -> RR* = ( Base ` ( mulGrp ` RR*s ) ) )
5 xrsmul 
 |-  *e = ( .r ` RR*s )
6 1 5 mgpplusg 
 |-  *e = ( +g ` ( mulGrp ` RR*s ) )
7 6 a1i 
 |-  ( T. -> *e = ( +g ` ( mulGrp ` RR*s ) ) )
8 xmulcl 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x *e y ) e. RR* )
9 8 3adant1 
 |-  ( ( T. /\ x e. RR* /\ y e. RR* ) -> ( x *e y ) e. RR* )
10 xmulass 
 |-  ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) )
11 10 adantl 
 |-  ( ( T. /\ ( x e. RR* /\ y e. RR* /\ z e. RR* ) ) -> ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) )
12 1re 
 |-  1 e. RR
13 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
14 12 13 mp1i 
 |-  ( T. -> 1 e. RR* )
15 xmullid 
 |-  ( x e. RR* -> ( 1 *e x ) = x )
16 15 adantl 
 |-  ( ( T. /\ x e. RR* ) -> ( 1 *e x ) = x )
17 xmulrid 
 |-  ( x e. RR* -> ( x *e 1 ) = x )
18 17 adantl 
 |-  ( ( T. /\ x e. RR* ) -> ( x *e 1 ) = x )
19 4 7 9 11 14 16 18 ismndd 
 |-  ( T. -> ( mulGrp ` RR*s ) e. Mnd )
20 xmulcom 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x *e y ) = ( y *e x ) )
21 20 3adant1 
 |-  ( ( T. /\ x e. RR* /\ y e. RR* ) -> ( x *e y ) = ( y *e x ) )
22 4 7 19 21 iscmnd 
 |-  ( T. -> ( mulGrp ` RR*s ) e. CMnd )
23 22 mptru 
 |-  ( mulGrp ` RR*s ) e. CMnd