Theorem xrge0cmn

Description: The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2	1	xrs1cmn	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd
3	1	xrge0subm	⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
4		xrex	⊢ ℝ* ∈ V
5	4	difexi	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
6		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
7		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
8	1 7	ressbas2	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) )
9	6 8	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
10	9	submss	⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) )
11	3 10	ax-mp	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
12		ressabs	⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
13	5 11 12	mp2an	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
14	13	eqcomi	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
15	14	submmnd	⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
16	3 15	ax-mp	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
17	14	subcmn	⊢ ( ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
18	2 16 17	mp2an	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd