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 ‘ ℝ*𝑠 ) ∈ 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 xmullid ⊢ ( 𝑥 ∈ ℝ* → ( 1 ·e 𝑥 ) = 𝑥 )
16 15 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ) → ( 1 ·e 𝑥 ) = 𝑥 )
17 xmulrid ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ·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