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		xmulid2	|- ( x e. RR* -> ( 1 *e x ) = x )
16	15	adantl	|- ( ( T. /\ x e. RR* ) -> ( 1 *e x ) = x )
17		xmulid1	|- ( 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