Metamath Proof Explorer

Theorem gsumge0cl

Description: Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses gsumge0cl.1 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
gsumge0cl.2 
|- ( ph -> X e. V )
gsumge0cl.3 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
gsumge0cl.4 
|- ( ph -> F finSupp 0 )
Assertion gsumge0cl 
|- ( ph -> ( G gsum F ) e. ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 gsumge0cl.1 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 gsumge0cl.2 
 |-  ( ph -> X e. V )
3 gsumge0cl.3 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
4 gsumge0cl.4 
 |-  ( ph -> F finSupp 0 )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 df-ss 
 |-  ( ( 0 [,] +oo ) C_ RR* <-> ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo ) )
7 5 6 mpbi 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo )
8 7 eqcomi 
 |-  ( 0 [,] +oo ) = ( ( 0 [,] +oo ) i^i RR* )
9 ovex 
 |-  ( 0 [,] +oo ) e. _V
10 xrsbas 
 |-  RR* = ( Base ` RR*s )
11 1 10 ressbas 
 |-  ( ( 0 [,] +oo ) e. _V -> ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` G ) )
12 9 11 ax-mp 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` G )
13 8 12 eqtri 
 |-  ( 0 [,] +oo ) = ( Base ` G )
14 eqid 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
15 14 xrs1cmn 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) e. CMnd
16 cmnmnd 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) e. CMnd -> ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd )
17 15 16 ax-mp 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd
18 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
19 1 18 eqeltri 
 |-  G e. CMnd
20 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
21 19 20 ax-mp 
 |-  G e. Mnd
22 17 21 pm3.2i 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd /\ G e. Mnd )
23 eliccxr 
 |-  ( x e. ( 0 [,] +oo ) -> x e. RR* )
24 mnfxr 
 |-  -oo e. RR*
25 24 a1i 
 |-  ( x e. ( 0 [,] +oo ) -> -oo e. RR* )
26 0xr 
 |-  0 e. RR*
27 26 a1i 
 |-  ( x e. ( 0 [,] +oo ) -> 0 e. RR* )
28 mnflt0 
 |-  -oo < 0
29 28 a1i 
 |-  ( x e. ( 0 [,] +oo ) -> -oo < 0 )
30 pnfxr 
 |-  +oo e. RR*
31 30 a1i 
 |-  ( x e. ( 0 [,] +oo ) -> +oo e. RR* )
32 id 
 |-  ( x e. ( 0 [,] +oo ) -> x e. ( 0 [,] +oo ) )
33 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ x e. ( 0 [,] +oo ) ) -> 0 <_ x )
34 27 31 32 33 syl3anc 
 |-  ( x e. ( 0 [,] +oo ) -> 0 <_ x )
35 25 27 23 29 34 xrltletrd 
 |-  ( x e. ( 0 [,] +oo ) -> -oo < x )
36 25 23 35 xrgtned 
 |-  ( x e. ( 0 [,] +oo ) -> x =/= -oo )
37 nelsn 
 |-  ( x =/= -oo -> -. x e. { -oo } )
38 36 37 syl 
 |-  ( x e. ( 0 [,] +oo ) -> -. x e. { -oo } )
39 23 38 eldifd 
 |-  ( x e. ( 0 [,] +oo ) -> x e. ( RR* \ { -oo } ) )
40 39 rgen 
 |-  A. x e. ( 0 [,] +oo ) x e. ( RR* \ { -oo } )
41 dfss3 
 |-  ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) <-> A. x e. ( 0 [,] +oo ) x e. ( RR* \ { -oo } ) )
42 40 41 mpbir 
 |-  ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
43 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
44 42 43 pm3.2i 
 |-  ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) /\ 0 e. ( 0 [,] +oo ) )
45 difss 
 |-  ( RR* \ { -oo } ) C_ RR*
46 14 10 ressbas2 
 |-  ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) ) )
47 45 46 ax-mp 
 |-  ( RR* \ { -oo } ) = ( Base ` ( RR*s |`s ( RR* \ { -oo } ) ) )
48 14 xrs10 
 |-  0 = ( 0g ` ( RR*s |`s ( RR* \ { -oo } ) ) )
49 xrex 
 |-  RR* e. _V
50 difexg 
 |-  ( RR* e. _V -> ( RR* \ { -oo } ) e. _V )
51 49 50 ax-mp 
 |-  ( RR* \ { -oo } ) e. _V
52 44 simpli 
 |-  ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
53 ressabs 
 |-  ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) )
54 51 52 53 mp2an 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
55 1 eqcomi 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = G
56 54 55 eqtr2i 
 |-  G = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
57 47 48 56 submnd0 
 |-  ( ( ( ( RR*s |`s ( RR* \ { -oo } ) ) e. Mnd /\ G e. Mnd ) /\ ( ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) /\ 0 e. ( 0 [,] +oo ) ) ) -> 0 = ( 0g ` G ) )
58 22 44 57 mp2an 
 |-  0 = ( 0g ` G )
59 19 a1i 
 |-  ( ph -> G e. CMnd )
60 13 58 59 2 3 4 gsumcl 
 |-  ( ph -> ( G gsum F ) e. ( 0 [,] +oo ) )