Metamath Proof Explorer

Theorem sge0tsms

Description: sum^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0tsms.g 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
sge0tsms.x 
|- ( ph -> X e. V )
sge0tsms.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion sge0tsms 
|- ( ph -> ( sum^ ` F ) e. ( G tsums F ) )

Proof

Step Hyp Ref Expression
1 sge0tsms.g 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 sge0tsms.x 
 |-  ( ph -> X e. V )
3 sge0tsms.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
4 eqid 
 |-  sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < )
5 4 a1i 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) )
6 xrltso 
 |-  < Or RR*
7 6 supex 
 |-  sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. _V
8 7 a1i 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. _V )
9 elsng 
 |-  ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. _V -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. { sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } <-> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) ) )
10 8 9 syl 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. { sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } <-> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) ) )
11 5 10 mpbird 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. { sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } )
12 2 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> X e. V )
13 3 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
14 simpr 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
15 12 13 14 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = +oo )
16 3 ffnd 
 |-  ( ph -> F Fn X )
17 16 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> F Fn X )
18 fvelrnb 
 |-  ( F Fn X -> ( +oo e. ran F <-> E. y e. X ( F ` y ) = +oo ) )
19 17 18 syl 
 |-  ( ( ph /\ +oo e. ran F ) -> ( +oo e. ran F <-> E. y e. X ( F ` y ) = +oo ) )
20 14 19 mpbid 
 |-  ( ( ph /\ +oo e. ran F ) -> E. y e. X ( F ` y ) = +oo )
21 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
22 simpr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. ( ~P X i^i Fin ) )
23 3 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
24 elinel1 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. ~P X )
25 elpwi 
 |-  ( x e. ~P X -> x C_ X )
26 24 25 syl 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
27 26 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
28 fssres 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x C_ X ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
29 23 27 28 syl2anc 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
30 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
31 30 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
32 0red 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> 0 e. RR )
33 29 31 32 fdmfifsupp 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) finSupp 0 )
34 1 22 29 33 gsumge0cl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( G gsum ( F |` x ) ) e. ( 0 [,] +oo ) )
35 21 34 sselid 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( G gsum ( F |` x ) ) e. RR* )
36 35 ralrimiva 
 |-  ( ph -> A. x e. ( ~P X i^i Fin ) ( G gsum ( F |` x ) ) e. RR* )
37 36 3ad2ant1 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> A. x e. ( ~P X i^i Fin ) ( G gsum ( F |` x ) ) e. RR* )
38 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) = ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) )
39 38 rnmptss 
 |-  ( A. x e. ( ~P X i^i Fin ) ( G gsum ( F |` x ) ) e. RR* -> ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) C_ RR* )
40 37 39 syl 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) C_ RR* )
41 snelpwi 
 |-  ( y e. X -> { y } e. ~P X )
42 snfi 
 |-  { y } e. Fin
43 42 a1i 
 |-  ( y e. X -> { y } e. Fin )
44 41 43 elind 
 |-  ( y e. X -> { y } e. ( ~P X i^i Fin ) )
45 44 3ad2ant2 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> { y } e. ( ~P X i^i Fin ) )
46 3 adantr 
 |-  ( ( ph /\ y e. X ) -> F : X --> ( 0 [,] +oo ) )
47 snssi 
 |-  ( y e. X -> { y } C_ X )
48 47 adantl 
 |-  ( ( ph /\ y e. X ) -> { y } C_ X )
49 46 48 fssresd 
 |-  ( ( ph /\ y e. X ) -> ( F |` { y } ) : { y } --> ( 0 [,] +oo ) )
50 49 feqmptd 
 |-  ( ( ph /\ y e. X ) -> ( F |` { y } ) = ( x e. { y } |-> ( ( F |` { y } ) ` x ) ) )
51 fvres 
 |-  ( x e. { y } -> ( ( F |` { y } ) ` x ) = ( F ` x ) )
52 51 mpteq2ia 
 |-  ( x e. { y } |-> ( ( F |` { y } ) ` x ) ) = ( x e. { y } |-> ( F ` x ) )
53 52 a1i 
 |-  ( ( ph /\ y e. X ) -> ( x e. { y } |-> ( ( F |` { y } ) ` x ) ) = ( x e. { y } |-> ( F ` x ) ) )
54 50 53 eqtrd 
 |-  ( ( ph /\ y e. X ) -> ( F |` { y } ) = ( x e. { y } |-> ( F ` x ) ) )
55 54 oveq2d 
 |-  ( ( ph /\ y e. X ) -> ( G gsum ( F |` { y } ) ) = ( G gsum ( x e. { y } |-> ( F ` x ) ) ) )
56 55 3adant3 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( G gsum ( F |` { y } ) ) = ( G gsum ( x e. { y } |-> ( F ` x ) ) ) )
57 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
58 1 57 eqeltri 
 |-  G e. CMnd
59 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
60 58 59 ax-mp 
 |-  G e. Mnd
61 60 a1i 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> G e. Mnd )
62 simp2 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> y e. X )
63 3 ffvelcdmda 
 |-  ( ( ph /\ y e. X ) -> ( F ` y ) e. ( 0 [,] +oo ) )
64 63 3adant3 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( F ` y ) e. ( 0 [,] +oo ) )
65 dfss2 
 |-  ( ( 0 [,] +oo ) C_ RR* <-> ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo ) )
66 21 65 mpbi 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo )
67 66 eqcomi 
 |-  ( 0 [,] +oo ) = ( ( 0 [,] +oo ) i^i RR* )
68 ovex 
 |-  ( 0 [,] +oo ) e. _V
69 xrsbas 
 |-  RR* = ( Base ` RR*s )
70 1 69 ressbas 
 |-  ( ( 0 [,] +oo ) e. _V -> ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` G ) )
71 68 70 ax-mp 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` G )
72 67 71 eqtri 
 |-  ( 0 [,] +oo ) = ( Base ` G )
73 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
74 72 73 gsumsn 
 |-  ( ( G e. Mnd /\ y e. X /\ ( F ` y ) e. ( 0 [,] +oo ) ) -> ( G gsum ( x e. { y } |-> ( F ` x ) ) ) = ( F ` y ) )
75 61 62 64 74 syl3anc 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( G gsum ( x e. { y } |-> ( F ` x ) ) ) = ( F ` y ) )
76 simp3 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( F ` y ) = +oo )
77 56 75 76 3eqtrrd 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo = ( G gsum ( F |` { y } ) ) )
78 reseq2 
 |-  ( x = { y } -> ( F |` x ) = ( F |` { y } ) )
79 78 oveq2d 
 |-  ( x = { y } -> ( G gsum ( F |` x ) ) = ( G gsum ( F |` { y } ) ) )
80 79 rspceeqv 
 |-  ( ( { y } e. ( ~P X i^i Fin ) /\ +oo = ( G gsum ( F |` { y } ) ) ) -> E. x e. ( ~P X i^i Fin ) +oo = ( G gsum ( F |` x ) ) )
81 45 77 80 syl2anc 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> E. x e. ( ~P X i^i Fin ) +oo = ( G gsum ( F |` x ) ) )
82 pnfxr 
 |-  +oo e. RR*
83 82 a1i 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo e. RR* )
84 38 elrnmpt 
 |-  ( +oo e. RR* -> ( +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) +oo = ( G gsum ( F |` x ) ) ) )
85 83 84 syl 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) +oo = ( G gsum ( F |` x ) ) ) )
86 81 85 mpbird 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) )
87 supxrpnf 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) C_ RR* /\ +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo )
88 40 86 87 syl2anc 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo )
89 88 3exp 
 |-  ( ph -> ( y e. X -> ( ( F ` y ) = +oo -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo ) ) )
90 89 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> ( y e. X -> ( ( F ` y ) = +oo -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo ) ) )
91 90 rexlimdv 
 |-  ( ( ph /\ +oo e. ran F ) -> ( E. y e. X ( F ` y ) = +oo -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo ) )
92 20 91 mpd 
 |-  ( ( ph /\ +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = +oo )
93 15 92 eqtr4d 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) )
94 2 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> X e. V )
95 3 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
96 simpr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> -. +oo e. ran F )
97 95 96 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,) +oo ) )
98 94 97 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
99 23 27 feqresmpt 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) = ( y e. x |-> ( F ` y ) ) )
100 99 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) = ( y e. x |-> ( F ` y ) ) )
101 100 oveq2d 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( G gsum ( F |` x ) ) = ( G gsum ( y e. x |-> ( F ` y ) ) ) )
102 1 fveq2i 
 |-  ( +g ` G ) = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
103 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
104 xrsadd 
 |-  +e = ( +g ` RR*s )
105 103 104 ressplusg 
 |-  ( ( 0 [,] +oo ) e. _V -> +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
106 68 105 ax-mp 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
107 106 eqcomi 
 |-  ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) ) = +e
108 102 107 eqtr2i 
 |-  +e = ( +g ` G )
109 1 oveq1i 
 |-  ( G |`s ( 0 [,) +oo ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) )
110 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
111 68 110 pm3.2i 
 |-  ( ( 0 [,] +oo ) e. _V /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
112 ressabs 
 |-  ( ( ( 0 [,] +oo ) e. _V /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( 0 [,) +oo ) ) )
113 111 112 ax-mp 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( 0 [,) +oo ) )
114 109 113 eqtr2i 
 |-  ( RR*s |`s ( 0 [,) +oo ) ) = ( G |`s ( 0 [,) +oo ) )
115 58 elexi 
 |-  G e. _V
116 115 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> G e. _V )
117 simpr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> x e. ( ~P X i^i Fin ) )
118 110 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
119 0xr 
 |-  0 e. RR*
120 119 a1i 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> 0 e. RR* )
121 82 a1i 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> +oo e. RR* )
122 95 ad2antrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,] +oo ) )
123 26 sselda 
 |-  ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. X )
124 123 adantll 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
125 122 124 ffvelcdmd 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,] +oo ) )
126 21 125 sselid 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR* )
127 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` y ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` y ) )
128 120 121 125 127 syl3anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> 0 <_ ( F ` y ) )
129 id 
 |-  ( ( F ` y ) = +oo -> ( F ` y ) = +oo )
130 129 eqcomd 
 |-  ( ( F ` y ) = +oo -> +oo = ( F ` y ) )
131 130 adantl 
 |-  ( ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ ( F ` y ) = +oo ) -> +oo = ( F ` y ) )
132 3 ffund 
 |-  ( ph -> Fun F )
133 132 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> Fun F )
134 22 123 sylan 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
135 3 fdmd 
 |-  ( ph -> dom F = X )
136 135 eqcomd 
 |-  ( ph -> X = dom F )
137 136 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> X = dom F )
138 134 137 eleqtrd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. dom F )
139 fvelrn 
 |-  ( ( Fun F /\ y e. dom F ) -> ( F ` y ) e. ran F )
140 133 138 139 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ran F )
141 140 adantr 
 |-  ( ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ ( F ` y ) = +oo ) -> ( F ` y ) e. ran F )
142 131 141 eqeltrd 
 |-  ( ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ ( F ` y ) = +oo ) -> +oo e. ran F )
143 142 adantl3r 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ ( F ` y ) = +oo ) -> +oo e. ran F )
144 96 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ ( F ` y ) = +oo ) -> -. +oo e. ran F )
145 143 144 pm2.65da 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> -. ( F ` y ) = +oo )
146 145 neqned 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) =/= +oo )
147 ge0xrre 
 |-  ( ( ( F ` y ) e. ( 0 [,] +oo ) /\ ( F ` y ) =/= +oo ) -> ( F ` y ) e. RR )
148 125 146 147 syl2anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
149 148 ltpnfd 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) < +oo )
150 120 121 126 128 149 elicod 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
151 eqid 
 |-  ( y e. x |-> ( F ` y ) ) = ( y e. x |-> ( F ` y ) )
152 150 151 fmptd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( y e. x |-> ( F ` y ) ) : x --> ( 0 [,) +oo ) )
153 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
154 153 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> 0 e. ( 0 [,) +oo ) )
155 eliccxr 
 |-  ( y e. ( 0 [,] +oo ) -> y e. RR* )
156 xaddlid 
 |-  ( y e. RR* -> ( 0 +e y ) = y )
157 xaddrid 
 |-  ( y e. RR* -> ( y +e 0 ) = y )
158 156 157 jca 
 |-  ( y e. RR* -> ( ( 0 +e y ) = y /\ ( y +e 0 ) = y ) )
159 155 158 syl 
 |-  ( y e. ( 0 [,] +oo ) -> ( ( 0 +e y ) = y /\ ( y +e 0 ) = y ) )
160 159 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. ( 0 [,] +oo ) ) -> ( ( 0 +e y ) = y /\ ( y +e 0 ) = y ) )
161 72 108 114 116 117 118 152 154 160 gsumress 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( G gsum ( y e. x |-> ( F ` y ) ) ) = ( ( RR*s |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) )
162 rege0subm 
 |-  ( 0 [,) +oo ) e. ( SubMnd ` CCfld )
163 162 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( 0 [,) +oo ) e. ( SubMnd ` CCfld ) )
164 eqid 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( 0 [,) +oo ) )
165 117 163 152 164 gsumsubm 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( CCfld gsum ( y e. x |-> ( F ` y ) ) ) = ( ( CCfld |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) )
166 eqidd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( ( CCfld |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) = ( ( CCfld |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) )
167 vex 
 |-  x e. _V
168 167 mptex 
 |-  ( y e. x |-> ( F ` y ) ) e. _V
169 168 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( y e. x |-> ( F ` y ) ) e. _V )
170 ovexd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( CCfld |`s ( 0 [,) +oo ) ) e. _V )
171 ovexd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( RR*s |`s ( 0 [,) +oo ) ) e. _V )
172 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
173 ax-resscn 
 |-  RR C_ CC
174 172 173 sstri 
 |-  ( 0 [,) +oo ) C_ CC
175 cnfldbas 
 |-  CC = ( Base ` CCfld )
176 164 175 ressbas2 
 |-  ( ( 0 [,) +oo ) C_ CC -> ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
177 174 176 ax-mp 
 |-  ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) )
178 177 eqcomi 
 |-  ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( 0 [,) +oo )
179 110 21 sstri 
 |-  ( 0 [,) +oo ) C_ RR*
180 eqid 
 |-  ( RR*s |`s ( 0 [,) +oo ) ) = ( RR*s |`s ( 0 [,) +oo ) )
181 180 69 ressbas2 
 |-  ( ( 0 [,) +oo ) C_ RR* -> ( 0 [,) +oo ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
182 179 181 ax-mp 
 |-  ( 0 [,) +oo ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) )
183 178 182 eqtri 
 |-  ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) )
184 183 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( Base ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
185 rge0srg 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) e. SRing
186 185 a1i 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> ( CCfld |`s ( 0 [,) +oo ) ) e. SRing )
187 simpl 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
188 simpr 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
189 eqid 
 |-  ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) )
190 eqid 
 |-  ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) )
191 189 190 srgacl 
 |-  ( ( ( CCfld |`s ( 0 [,) +oo ) ) e. SRing /\ s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
192 186 187 188 191 syl3anc 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
193 192 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
194 172 a1i 
 |-  ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> ( 0 [,) +oo ) C_ RR )
195 id 
 |-  ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
196 195 178 eleqtrdi 
 |-  ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> s e. ( 0 [,) +oo ) )
197 194 196 sseldd 
 |-  ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> s e. RR )
198 197 adantr 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> s e. RR )
199 172 a1i 
 |-  ( t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> ( 0 [,) +oo ) C_ RR )
200 id 
 |-  ( t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
201 200 178 eleqtrdi 
 |-  ( t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> t e. ( 0 [,) +oo ) )
202 199 201 sseldd 
 |-  ( t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> t e. RR )
203 202 adantl 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> t e. RR )
204 rexadd 
 |-  ( ( s e. RR /\ t e. RR ) -> ( s +e t ) = ( s + t ) )
205 204 eqcomd 
 |-  ( ( s e. RR /\ t e. RR ) -> ( s + t ) = ( s +e t ) )
206 162 elexi 
 |-  ( 0 [,) +oo ) e. _V
207 cnfldadd 
 |-  + = ( +g ` CCfld )
208 164 207 ressplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
209 206 208 ax-mp 
 |-  + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) )
210 209 207 eqtr3i 
 |-  ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) = ( +g ` CCfld )
211 210 207 eqtr4i 
 |-  ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) = +
212 211 oveqi 
 |-  ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) = ( s + t )
213 212 a1i 
 |-  ( ( s e. RR /\ t e. RR ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) = ( s + t ) )
214 180 104 ressplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> +e = ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) )
215 206 214 ax-mp 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) )
216 215 eqcomi 
 |-  ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) = +e
217 216 oveqi 
 |-  ( s ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) t ) = ( s +e t )
218 217 a1i 
 |-  ( ( s e. RR /\ t e. RR ) -> ( s ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) t ) = ( s +e t ) )
219 205 213 218 3eqtr4d 
 |-  ( ( s e. RR /\ t e. RR ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) = ( s ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) t ) )
220 198 203 219 syl2anc 
 |-  ( ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) = ( s ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) t ) )
221 220 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ ( s e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) /\ t e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) ) -> ( s ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) t ) = ( s ( +g ` ( RR*s |`s ( 0 [,) +oo ) ) ) t ) )
222 funmpt 
 |-  Fun ( y e. x |-> ( F ` y ) )
223 222 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> Fun ( y e. x |-> ( F ` y ) ) )
224 150 177 eleqtrdi 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
225 224 ralrimiva 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> A. y e. x ( F ` y ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
226 151 rnmptss 
 |-  ( A. y e. x ( F ` y ) e. ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) -> ran ( y e. x |-> ( F ` y ) ) C_ ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
227 225 226 syl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ran ( y e. x |-> ( F ` y ) ) C_ ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
228 169 170 171 184 193 221 223 227 gsumpropd2 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( ( CCfld |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) = ( ( RR*s |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) )
229 165 166 228 3eqtrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( CCfld gsum ( y e. x |-> ( F ` y ) ) ) = ( ( RR*s |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) )
230 30 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
231 148 recnd 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. CC )
232 230 231 gsumfsum 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( CCfld gsum ( y e. x |-> ( F ` y ) ) ) = sum_ y e. x ( F ` y ) )
233 229 232 eqtr3d 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,) +oo ) ) gsum ( y e. x |-> ( F ` y ) ) ) = sum_ y e. x ( F ` y ) )
234 101 161 233 3eqtrrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( G gsum ( F |` x ) ) )
235 234 mpteq2dva 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) )
236 235 rneqd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) )
237 236 supeq1d 
 |-  ( ( ph /\ -. +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) )
238 98 237 eqtrd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) )
239 93 238 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) )
240 1 2 3 4 xrge0tsms 
 |-  ( ph -> ( G tsums F ) = { sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } )
241 239 240 eleq12d 
 |-  ( ph -> ( ( sum^ ` F ) e. ( G tsums F ) <-> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. { sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } ) )
242 11 241 mpbird 
 |-  ( ph -> ( sum^ ` F ) e. ( G tsums F ) )