This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfss2 ⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* ↔ ( ( ℝ* ∖ { -∞ } ) ∩ ℝ* ) = ( ℝ* ∖ { -∞ } ) )
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 [,] +∞ ) ) )