Metamath Proof Explorer

Theorem sge0split

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0split.a 
|- ( ph -> A e. V )
sge0split.b 
|- ( ph -> B e. W )
sge0split.u 
|- U = ( A u. B )
sge0split.in0 
|- ( ph -> ( A i^i B ) = (/) )
sge0split.f 
|- ( ph -> F : U --> ( 0 [,] +oo ) )
Assertion sge0split 
|- ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0split.a 
 |-  ( ph -> A e. V )
2 sge0split.b 
 |-  ( ph -> B e. W )
3 sge0split.u 
 |-  U = ( A u. B )
4 sge0split.in0 
 |-  ( ph -> ( A i^i B ) = (/) )
5 sge0split.f 
 |-  ( ph -> F : U --> ( 0 [,] +oo ) )
6 1 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> A e. V )
7 2 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> B e. W )
8 4 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( A i^i B ) = (/) )
9 5 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> F : U --> ( 0 [,] +oo ) )
10 simpr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) e. RR )
11 6 7 3 8 9 10 sge0resplit 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
12 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
13 1 2 12 syl2anc 
 |-  ( ph -> ( A u. B ) e. _V )
14 3 13 eqeltrid 
 |-  ( ph -> U e. _V )
15 14 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> U e. _V )
16 15 9 10 sge0ssre 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` A ) ) e. RR )
17 15 9 10 sge0ssre 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` B ) ) e. RR )
18 rexadd 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR /\ ( sum^ ` ( F |` B ) ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
19 16 17 18 syl2anc 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
20 19 eqcomd 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
21 11 20 eqtrd 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
22 simpl 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ph )
23 simpr 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> -. ( sum^ ` F ) e. RR )
24 14 5 sge0repnf 
 |-  ( ph -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
25 24 adantr 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
26 23 25 mtbid 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> -. -. ( sum^ ` F ) = +oo )
27 26 notnotrd 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = +oo )
28 14 5 sge0xrcl 
 |-  ( ph -> ( sum^ ` F ) e. RR* )
29 28 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. RR* )
30 ssun1 
 |-  A C_ ( A u. B )
31 30 3 sseqtrri 
 |-  A C_ U
32 31 a1i 
 |-  ( ph -> A C_ U )
33 5 32 fssresd 
 |-  ( ph -> ( F |` A ) : A --> ( 0 [,] +oo ) )
34 1 33 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) e. RR* )
35 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
36 ssun2 
 |-  B C_ ( A u. B )
37 36 3 sseqtrri 
 |-  B C_ U
38 37 a1i 
 |-  ( ph -> B C_ U )
39 5 38 fssresd 
 |-  ( ph -> ( F |` B ) : B --> ( 0 [,] +oo ) )
40 2 39 sge0cl 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) e. ( 0 [,] +oo ) )
41 35 40 sselid 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) e. RR* )
42 34 41 xaddcld 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* )
43 42 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* )
44 pnfxr 
 |-  +oo e. RR*
45 eqid 
 |-  +oo = +oo
46 xreqle 
 |-  ( ( +oo e. RR* /\ +oo = +oo ) -> +oo <_ +oo )
47 44 45 46 mp2an 
 |-  +oo <_ +oo
48 47 a1i 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo <_ +oo )
49 14 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> U e. _V )
50 5 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> F : U --> ( 0 [,] +oo ) )
51 rnresss 
 |-  ran ( F |` A ) C_ ran F
52 51 sseli 
 |-  ( +oo e. ran ( F |` A ) -> +oo e. ran F )
53 52 adantl 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo e. ran F )
54 49 50 53 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) = +oo )
55 xrge0neqmnf 
 |-  ( ( sum^ ` ( F |` B ) ) e. ( 0 [,] +oo ) -> ( sum^ ` ( F |` B ) ) =/= -oo )
56 40 55 syl 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) =/= -oo )
57 xaddpnf2 
 |-  ( ( ( sum^ ` ( F |` B ) ) e. RR* /\ ( sum^ ` ( F |` B ) ) =/= -oo ) -> ( +oo +e ( sum^ ` ( F |` B ) ) ) = +oo )
58 41 56 57 syl2anc 
 |-  ( ph -> ( +oo +e ( sum^ ` ( F |` B ) ) ) = +oo )
59 58 eqcomd 
 |-  ( ph -> +oo = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
60 59 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
61 1 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> A e. V )
62 33 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
63 simpr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo e. ran ( F |` A ) )
64 61 62 63 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) = +oo )
65 64 oveq1d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
66 60 54 65 3eqtr4d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
67 66 54 eqtr3d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = +oo )
68 54 67 breq12d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <-> +oo <_ +oo ) )
69 48 68 mpbird 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
70 47 a1i 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo <_ +oo )
71 14 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> U e. _V )
72 5 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,] +oo ) )
73 rnresss 
 |-  ran ( F |` B ) C_ ran F
74 73 sseli 
 |-  ( +oo e. ran ( F |` B ) -> +oo e. ran F )
75 74 adantl 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo e. ran F )
76 71 72 75 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) = +oo )
77 2 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> B e. W )
78 39 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
79 simpr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo e. ran ( F |` B ) )
80 77 78 79 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = +oo )
81 80 oveq2d 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) +e +oo ) )
82 1 33 sge0cl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) e. ( 0 [,] +oo ) )
83 xrge0neqmnf 
 |-  ( ( sum^ ` ( F |` A ) ) e. ( 0 [,] +oo ) -> ( sum^ ` ( F |` A ) ) =/= -oo )
84 82 83 syl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) =/= -oo )
85 xaddpnf1 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR* /\ ( sum^ ` ( F |` A ) ) =/= -oo ) -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
86 34 84 85 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
87 86 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
88 81 87 eqtrd 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = +oo )
89 76 88 breq12d 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <-> +oo <_ +oo ) )
90 70 89 mpbird 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
91 90 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
92 vex 
 |-  z e. _V
93 eqid 
 |-  ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
94 93 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) ) )
95 92 94 ax-mp 
 |-  ( z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) )
96 95 bilani 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) )
97 simp3 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> z = sum_ y e. x ( F ` y ) )
98 inss1 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( x i^i A )
99 inss2 
 |-  ( x i^i A ) C_ A
100 98 99 sstri 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ A
101 inss2 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( x i^i B )
102 inss2 
 |-  ( x i^i B ) C_ B
103 101 102 sstri 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ B
104 100 103 ssini 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( A i^i B )
105 104 a1i 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( A i^i B ) )
106 105 4 sseqtrd 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) C_ (/) )
107 ss0 
 |-  ( ( ( x i^i A ) i^i ( x i^i B ) ) C_ (/) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
108 106 107 syl 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
109 108 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
110 indi 
 |-  ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( x i^i B ) )
111 110 eqcomi 
 |-  ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) )
112 111 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) ) )
113 3 eqcomi 
 |-  ( A u. B ) = U
114 113 ineq2i 
 |-  ( x i^i ( A u. B ) ) = ( x i^i U )
115 114 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i ( A u. B ) ) = ( x i^i U ) )
116 elinel1 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. ~P U )
117 elpwi 
 |-  ( x e. ~P U -> x C_ U )
118 116 117 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x C_ U )
119 dfss2 
 |-  ( x C_ U <-> ( x i^i U ) = x )
120 119 biimpi 
 |-  ( x C_ U -> ( x i^i U ) = x )
121 118 120 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i U ) = x )
122 112 115 121 3eqtrrd 
 |-  ( x e. ( ~P U i^i Fin ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
123 122 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
124 elinel2 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. Fin )
125 124 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> x e. Fin )
126 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
127 5 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,] +oo ) )
128 pm4.56 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) <-> -. ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
129 128 biimpi 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) -> -. ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
130 elun 
 |-  ( +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) <-> ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
131 129 130 sylnibr 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) )
132 131 adantll 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) )
133 rnresun 
 |-  ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )
134 133 eqcomi 
 |-  ( ran ( F |` A ) u. ran ( F |` B ) ) = ran ( F |` ( A u. B ) )
135 134 a1i 
 |-  ( ph -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran ( F |` ( A u. B ) ) )
136 113 reseq2i 
 |-  ( F |` ( A u. B ) ) = ( F |` U )
137 136 rneqi 
 |-  ran ( F |` ( A u. B ) ) = ran ( F |` U )
138 137 a1i 
 |-  ( ph -> ran ( F |` ( A u. B ) ) = ran ( F |` U ) )
139 ffn 
 |-  ( F : U --> ( 0 [,] +oo ) -> F Fn U )
140 fnresdm 
 |-  ( F Fn U -> ( F |` U ) = F )
141 5 139 140 3syl 
 |-  ( ph -> ( F |` U ) = F )
142 141 rneqd 
 |-  ( ph -> ran ( F |` U ) = ran F )
143 135 138 142 3eqtrd 
 |-  ( ph -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran F )
144 143 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran F )
145 132 144 neleqtrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ran F )
146 127 145 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,) +oo ) )
147 146 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> F : U --> ( 0 [,) +oo ) )
148 118 adantr 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> x C_ U )
149 simpr 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. x )
150 148 149 sseldd 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. U )
151 150 adantll 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> y e. U )
152 147 151 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
153 126 152 sselid 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
154 153 recnd 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. CC )
155 109 123 125 154 fsumsplit 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
156 infi 
 |-  ( x e. Fin -> ( x i^i A ) e. Fin )
157 124 156 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. Fin )
158 157 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) e. Fin )
159 simpl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) )
160 elinel1 
 |-  ( y e. ( x i^i A ) -> y e. x )
161 160 adantl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> y e. x )
162 159 161 153 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( F ` y ) e. RR )
163 158 162 fsumrecl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. RR )
164 infi 
 |-  ( x e. Fin -> ( x i^i B ) e. Fin )
165 124 164 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) e. Fin )
166 165 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) e. Fin )
167 simpl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) )
168 elinel1 
 |-  ( y e. ( x i^i B ) -> y e. x )
169 168 adantl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> y e. x )
170 167 169 153 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( F ` y ) e. RR )
171 166 170 fsumrecl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. RR )
172 rexadd 
 |-  ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
173 163 171 172 syl2anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
174 173 eqcomd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) )
175 155 174 eqtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) )
176 ressxr 
 |-  RR C_ RR*
177 176 163 sselid 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. RR* )
178 176 171 sselid 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. RR* )
179 1 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> A e. V )
180 33 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
181 simpr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> -. +oo e. ran ( F |` A ) )
182 180 181 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,) +oo ) )
183 179 182 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
184 183 eqcomd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) = ( sum^ ` ( F |` A ) ) )
185 34 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) e. RR* )
186 184 185 eqeltrd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* )
187 186 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* )
188 2 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> B e. W )
189 39 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
190 simpr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ran ( F |` B ) )
191 189 190 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,) +oo ) )
192 188 191 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
193 192 eqcomd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) = ( sum^ ` ( F |` B ) ) )
194 41 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) e. RR* )
195 193 194 eqeltrd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* )
196 195 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* )
197 187 196 jca 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) )
198 197 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) )
199 177 178 198 jca31 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR* /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR* ) /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) ) )
200 179 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> A e. V )
201 180 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
202 181 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> -. +oo e. ran ( F |` A ) )
203 201 202 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` A ) : A --> ( 0 [,) +oo ) )
204 99 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) C_ A )
205 157 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) e. Fin )
206 200 203 204 205 fsumlesge0 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) <_ ( sum^ ` ( F |` A ) ) )
207 99 sseli 
 |-  ( y e. ( x i^i A ) -> y e. A )
208 fvres 
 |-  ( y e. A -> ( ( F |` A ) ` y ) = ( F ` y ) )
209 207 208 syl 
 |-  ( y e. ( x i^i A ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
210 209 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
211 210 sumeq2dv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) = sum_ y e. ( x i^i A ) ( F ` y ) )
212 183 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
213 211 212 breq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) <_ ( sum^ ` ( F |` A ) ) <-> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) ) )
214 206 213 mpbid 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
215 214 adantlr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
216 188 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> B e. W )
217 189 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
218 190 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> -. +oo e. ran ( F |` B ) )
219 217 218 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` B ) : B --> ( 0 [,) +oo ) )
220 102 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) C_ B )
221 165 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) e. Fin )
222 216 219 220 221 fsumlesge0 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) <_ ( sum^ ` ( F |` B ) ) )
223 102 sseli 
 |-  ( y e. ( x i^i B ) -> y e. B )
224 fvres 
 |-  ( y e. B -> ( ( F |` B ) ` y ) = ( F ` y ) )
225 223 224 syl 
 |-  ( y e. ( x i^i B ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
226 225 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
227 226 sumeq2dv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) = sum_ y e. ( x i^i B ) ( F ` y ) )
228 192 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
229 227 228 breq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) <_ ( sum^ ` ( F |` B ) ) <-> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
230 222 229 mpbid 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
231 230 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
232 215 231 jca 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) /\ sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
233 xle2add 
 |-  ( ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR* /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR* ) /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) ) -> ( ( sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) /\ sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
234 199 232 233 sylc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
235 175 234 eqbrtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
236 235 3adant3 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> sum_ y e. x ( F ` y ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
237 97 236 eqbrtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
238 237 3exp 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( x e. ( ~P U i^i Fin ) -> ( z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) ) )
239 238 rexlimdv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
240 239 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
241 96 240 mpd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
242 241 ralrimiva 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
243 146 sge0rnre 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
244 176 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> RR C_ RR* )
245 243 244 sstrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
246 187 196 xaddcld 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) e. RR* )
247 supxrleub 
 |-  ( ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) e. RR* ) -> ( sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) <-> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
248 245 246 247 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) <-> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
249 242 248 mpbird 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
250 14 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> U e. _V )
251 250 146 sge0reval 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
252 183 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
253 192 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
254 252 253 oveq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
255 249 251 254 3brtr4d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
256 91 255 pm2.61dan 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
257 69 256 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
258 257 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
259 pnfge 
 |-  ( ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
260 42 259 syl 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
261 260 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
262 id 
 |-  ( ( sum^ ` F ) = +oo -> ( sum^ ` F ) = +oo )
263 262 eqcomd 
 |-  ( ( sum^ ` F ) = +oo -> +oo = ( sum^ ` F ) )
264 263 adantl 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> +oo = ( sum^ ` F ) )
265 261 264 breqtrd 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ ( sum^ ` F ) )
266 29 43 258 265 xrletrid 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
267 22 27 266 syl2anc 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
268 21 267 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )