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 ` ( RR*s |`s ( 0 [,] +oo ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
2 1 xrs1mnd 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd
3 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
4 cmnmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
5 3 4 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
6 mnflt0 
 |-  -oo < 0
7 mnfxr 
 |-  -oo e. RR*
8 0xr 
 |-  0 e. RR*
9 xrltnle 
 |-  ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
10 7 8 9 mp2an 
 |-  ( -oo < 0 <-> -. 0 <_ -oo )
11 6 10 mpbi 
 |-  -. 0 <_ -oo
12 11 intnan 
 |-  -. ( -oo e. RR* /\ 0 <_ -oo )
13 elxrge0 
 |-  ( -oo e. ( 0 [,] +oo ) <-> ( -oo e. RR* /\ 0 <_ -oo ) )
14 12 13 mtbir 
 |-  -. -oo e. ( 0 [,] +oo )
15 difsn 
 |-  ( -. -oo e. ( 0 [,] +oo ) -> ( ( 0 [,] +oo ) \ { -oo } ) = ( 0 [,] +oo ) )
16 14 15 ax-mp 
 |-  ( ( 0 [,] +oo ) \ { -oo } ) = ( 0 [,] +oo )
17 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
18 ssdif 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( ( 0 [,] +oo ) \ { -oo } ) C_ ( RR* \ { -oo } ) )
19 17 18 ax-mp 
 |-  ( ( 0 [,] +oo ) \ { -oo } ) C_ ( RR* \ { -oo } )
20 16 19 eqsstrri 
 |-  ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
21 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
22 difss 
 |-  ( RR* \ { -oo } ) C_ RR*
23 df-ss 
 |-  ( ( RR* \ { -oo } ) C_ RR* <-> ( ( RR* \ { -oo } ) i^i RR* ) = ( RR* \ { -oo } ) )
24 22 23 mpbi 
 |-  ( ( RR* \ { -oo } ) i^i RR* ) = ( RR* \ { -oo } )
25 xrex 
 |-  RR* e. _V
26 difexg 
 |-  ( RR* e. _V -> ( RR* \ { -oo } ) e. _V )
27 25 26 ax-mp 
 |-  ( RR* \ { -oo } ) e. _V
28 xrsbas 
 |-  RR* = ( Base ` RR*s )
29 1 28 ressbas 
 |-  ( ( RR* \ { -oo } ) e. _V -> ( ( RR* \ { -oo } ) i^i RR* ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) ) )
30 27 29 ax-mp 
 |-  ( ( RR* \ { -oo } ) i^i RR* ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) )
31 24 30 eqtr3i 
 |-  ( RR* \ { -oo } ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) )
32 1 xrs10 
 |-  0 = ( 0g ` ( RR*s |`s ( RR* \ { -oo } ) ) )
33 ovex 
 |-  ( 0 [,] +oo ) e. _V
34 ressress 
 |-  ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) e. _V ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( ( RR* \ { -oo } ) i^i ( 0 [,] +oo ) ) ) )
35 27 33 34 mp2an 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( ( RR* \ { -oo } ) i^i ( 0 [,] +oo ) ) )
36 dfss 
 |-  ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) <-> ( 0 [,] +oo ) = ( ( 0 [,] +oo ) i^i ( RR* \ { -oo } ) ) )
37 20 36 mpbi 
 |-  ( 0 [,] +oo ) = ( ( 0 [,] +oo ) i^i ( RR* \ { -oo } ) )
38 incom 
 |-  ( ( 0 [,] +oo ) i^i ( RR* \ { -oo } ) ) = ( ( RR* \ { -oo } ) i^i ( 0 [,] +oo ) )
39 37 38 eqtr2i 
 |-  ( ( RR* \ { -oo } ) i^i ( 0 [,] +oo ) ) = ( 0 [,] +oo )
40 39 oveq2i 
 |-  ( RR*s |`s ( ( RR* \ { -oo } ) i^i ( 0 [,] +oo ) ) ) = ( RR*s |`s ( 0 [,] +oo ) )
41 35 40 eqtr2i 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
42 31 32 41 submnd0 
 |-  ( ( ( ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd ) /\ ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) /\ 0 e. ( 0 [,] +oo ) ) ) -> 0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
43 2 5 20 21 42 mp4an 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )