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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | xrsbas | |
|
3 | 1 2 | mgpbas | |
4 | 3 | a1i | |
5 | xrsmul | |
|
6 | 1 5 | mgpplusg | |
7 | 6 | a1i | |
8 | xmulcl | |
|
9 | 8 | 3adant1 | |
10 | xmulass | |
|
11 | 10 | adantl | |
12 | 1re | |
|
13 | rexr | |
|
14 | 12 13 | mp1i | |
15 | xmulid2 | |
|
16 | 15 | adantl | |
17 | xmulid1 | |
|
18 | 17 | adantl | |
19 | 4 7 9 11 14 16 18 | ismndd | |
20 | xmulcom | |
|
21 | 20 | 3adant1 | |
22 | 4 7 19 21 | iscmnd | |
23 | 22 | mptru | |