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	⊢ ℝ* = ( Base ‘ ( mulGrp ‘ ℝ*𝑠 ) )
4	3	a1i	⊢ ( ⊤ → ℝ* = ( Base ‘ ( mulGrp ‘ ℝ*𝑠 ) ) )
5		xrsmul	⊢ ·e = ( .r ‘ ℝ*𝑠 )
6	1 5	mgpplusg	⊢ ·e = ( +g ‘ ( mulGrp ‘ ℝ*𝑠 ) )
7	6	a1i	⊢ ( ⊤ → ·e = ( +g ‘ ( mulGrp ‘ ℝ*𝑠 ) ) )
8		xmulcl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ·e 𝑦 ) ∈ ℝ* )
9	8	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ·e 𝑦 ) ∈ ℝ* )
10		xmulass	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 ·e 𝑦 ) ·e 𝑧 ) = ( 𝑥 ·e ( 𝑦 ·e 𝑧 ) ) )
11	10	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ) → ( ( 𝑥 ·e 𝑦 ) ·e 𝑧 ) = ( 𝑥 ·e ( 𝑦 ·e 𝑧 ) ) )
12		1re	⊢ 1 ∈ ℝ
13		rexr	⊢ ( 1 ∈ ℝ → 1 ∈ ℝ* )
14	12 13	mp1i	⊢ ( ⊤ → 1 ∈ ℝ* )
15		xmulid2	⊢ ( 𝑥 ∈ ℝ* → ( 1 ·e 𝑥 ) = 𝑥 )
16	15	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ) → ( 1 ·e 𝑥 ) = 𝑥 )
17		xmulid1	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ·e 1 ) = 𝑥 )
18	17	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 ·e 1 ) = 𝑥 )
19	4 7 9 11 14 16 18	ismndd	⊢ ( ⊤ → ( mulGrp ‘ ℝ*𝑠 ) ∈ Mnd )
20		xmulcom	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ·e 𝑦 ) = ( 𝑦 ·e 𝑥 ) )
21	20	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ·e 𝑦 ) = ( 𝑦 ·e 𝑥 ) )
22	4 7 19 21	iscmnd	⊢ ( ⊤ → ( mulGrp ‘ ℝ*𝑠 ) ∈ CMnd )
23	22	mptru	⊢ ( mulGrp ‘ ℝ*𝑠 ) ∈ CMnd