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	$$⊢{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}={\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}$$
2		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3	1 2	mgpbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}}$$
4	3	a1i	$$⊢\top \to {ℝ}^{*}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}}$$
5		xrsmul	$$⊢{\cdot }_{𝑒}={\cdot }_{{ℝ}_{𝑠}^{*}}$$
6	1 5	mgpplusg	$$⊢{\cdot }_{𝑒}={+}_{{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}}$$
7	6	a1i	$$⊢\top \to {\cdot }_{𝑒}={+}_{{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}}$$
8		xmulcl	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{\cdot }_{𝑒}y\in {ℝ}^{*}$$
9	8	3adant1	$$⊢\left(\top \wedge x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{\cdot }_{𝑒}y\in {ℝ}^{*}$$
10		xmulass	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\to \left(x{\cdot }_{𝑒}y\right){\cdot }_{𝑒}z=x{\cdot }_{𝑒}\left(y{\cdot }_{𝑒}z\right)$$
11	10	adantl	$$⊢\left(\top \wedge \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\right)\to \left(x{\cdot }_{𝑒}y\right){\cdot }_{𝑒}z=x{\cdot }_{𝑒}\left(y{\cdot }_{𝑒}z\right)$$
12		1re	$$⊢1\in ℝ$$
13		rexr	$$⊢1\in ℝ\to 1\in {ℝ}^{*}$$
14	12 13	mp1i	$$⊢\top \to 1\in {ℝ}^{*}$$
15		xmulid2	$$⊢x\in {ℝ}^{*}\to 1{\cdot }_{𝑒}x=x$$
16	15	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{*}\right)\to 1{\cdot }_{𝑒}x=x$$
17		xmulid1	$$⊢x\in {ℝ}^{*}\to x{\cdot }_{𝑒}1=x$$
18	17	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{*}\right)\to x{\cdot }_{𝑒}1=x$$
19	4 7 9 11 14 16 18	ismndd	$$⊢\top \to {\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}\in \mathrm{Mnd}$$
20		xmulcom	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{\cdot }_{𝑒}y=y{\cdot }_{𝑒}x$$
21	20	3adant1	$$⊢\left(\top \wedge x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{\cdot }_{𝑒}y=y{\cdot }_{𝑒}x$$
22	4 7 19 21	iscmnd	$$⊢\top \to {\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}\in \mathrm{CMnd}$$
23	22	mptru	$$⊢{\mathrm{mulGrp}}_{{ℝ}_{𝑠}^{*}}\in \mathrm{CMnd}$$