Theorem xrge00

Description: The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Assertion	xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2	1	xrs1mnd	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd
3		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
4		cmnmnd	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
5	3 4	ax-mp	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
6		mnflt0	⊢ -∞ < 0
7		mnfxr	⊢ -∞ ∈ ℝ*
8		0xr	⊢ 0 ∈ ℝ*
9		xrltnle	⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( -∞ < 0 ↔ ¬ 0 ≤ -∞ ) )
10	7 8 9	mp2an	⊢ ( -∞ < 0 ↔ ¬ 0 ≤ -∞ )
11	6 10	mpbi	⊢ ¬ 0 ≤ -∞
12	11	intnan	⊢ ¬ ( -∞ ∈ ℝ* ∧ 0 ≤ -∞ )
13		elxrge0	⊢ ( -∞ ∈ ( 0 [,] +∞ ) ↔ ( -∞ ∈ ℝ* ∧ 0 ≤ -∞ ) )
14	12 13	mtbir	⊢ ¬ -∞ ∈ ( 0 [,] +∞ )
15		difsn	⊢ ( ¬ -∞ ∈ ( 0 [,] +∞ ) → ( ( 0 [,] +∞ ) ∖ { -∞ } ) = ( 0 [,] +∞ ) )
16	14 15	ax-mp	⊢ ( ( 0 [,] +∞ ) ∖ { -∞ } ) = ( 0 [,] +∞ )
17		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
18		ssdif	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( ( 0 [,] +∞ ) ∖ { -∞ } ) ⊆ ( ℝ* ∖ { -∞ } ) )
19	17 18	ax-mp	⊢ ( ( 0 [,] +∞ ) ∖ { -∞ } ) ⊆ ( ℝ* ∖ { -∞ } )
20	16 19	eqsstrri	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
21		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
22		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
23		df-ss	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* ↔ ( ( ℝ* ∖ { -∞ } ) ∩ ℝ* ) = ( ℝ* ∖ { -∞ } ) )
24	22 23	mpbi	⊢ ( ( ℝ* ∖ { -∞ } ) ∩ ℝ* ) = ( ℝ* ∖ { -∞ } )
25		xrex	⊢ ℝ* ∈ V
26		difexg	⊢ ( ℝ* ∈ V → ( ℝ* ∖ { -∞ } ) ∈ V )
27	25 26	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
28		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
29	1 28	ressbas	⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → ( ( ℝ* ∖ { -∞ } ) ∩ ℝ* ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) )
30	27 29	ax-mp	⊢ ( ( ℝ* ∖ { -∞ } ) ∩ ℝ* ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
31	24 30	eqtr3i	⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
32	1	xrs10	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
33		ovex	⊢ ( 0 [,] +∞ ) ∈ V
34		ressress	⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ∈ V ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( ( ℝ* ∖ { -∞ } ) ∩ ( 0 [,] +∞ ) ) ) )
35	27 33 34	mp2an	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( ( ℝ* ∖ { -∞ } ) ∩ ( 0 [,] +∞ ) ) )
36		dfss	⊢ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ↔ ( 0 [,] +∞ ) = ( ( 0 [,] +∞ ) ∩ ( ℝ* ∖ { -∞ } ) ) )
37	20 36	mpbi	⊢ ( 0 [,] +∞ ) = ( ( 0 [,] +∞ ) ∩ ( ℝ* ∖ { -∞ } ) )
38		incom	⊢ ( ( 0 [,] +∞ ) ∩ ( ℝ* ∖ { -∞ } ) ) = ( ( ℝ* ∖ { -∞ } ) ∩ ( 0 [,] +∞ ) )
39	37 38	eqtr2i	⊢ ( ( ℝ* ∖ { -∞ } ) ∩ ( 0 [,] +∞ ) ) = ( 0 [,] +∞ )
40	39	oveq2i	⊢ ( ℝ*𝑠 ↾s ( ( ℝ* ∖ { -∞ } ) ∩ ( 0 [,] +∞ ) ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
41	35 40	eqtr2i	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
42	31 32 41	submnd0	⊢ ( ( ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ) ∧ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ) ) → 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) )
43	2 5 20 21 42	mp4an	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )