Metamath Proof Explorer

Theorem sge0resplit

Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 sge0resplit.a 
 |-  ( ph -> A e. V )
2 sge0resplit.b 
 |-  ( ph -> B e. W )
3 sge0resplit.u 
 |-  U = ( A u. B )
4 sge0resplit.in0 
 |-  ( ph -> ( A i^i B ) = (/) )
5 sge0resplit.f 
 |-  ( ph -> F : U --> ( 0 [,] +oo ) )
6 sge0resplit.re 
 |-  ( ph -> ( sum^ ` F ) e. RR )
7 ssun1 
 |-  A C_ ( A u. B )
8 3 eqcomi 
 |-  ( A u. B ) = U
9 7 8 sseqtri 
 |-  A C_ U
10 9 a1i 
 |-  ( ph -> A C_ U )
11 5 10 fssresd 
 |-  ( ph -> ( F |` A ) : A --> ( 0 [,] +oo ) )
12 3 a1i 
 |-  ( ph -> U = ( A u. B ) )
13 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
14 1 2 13 syl2anc 
 |-  ( ph -> ( A u. B ) e. _V )
15 12 14 eqeltrd 
 |-  ( ph -> U e. _V )
16 15 5 6 sge0ssre 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) e. RR )
17 1 11 16 sge0supre 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) = sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) )
18 17 16 eqeltrrd 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) e. RR )
19 ssun2 
 |-  B C_ ( A u. B )
20 19 8 sseqtri 
 |-  B C_ U
21 20 a1i 
 |-  ( ph -> B C_ U )
22 5 21 fssresd 
 |-  ( ph -> ( F |` B ) : B --> ( 0 [,] +oo ) )
23 15 5 6 sge0ssre 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) e. RR )
24 2 22 23 sge0supre 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) = sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) )
25 24 23 eqeltrrd 
 |-  ( ph -> sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) e. RR )
26 rexadd 
 |-  ( ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) e. RR /\ sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) e. RR ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) +e sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) + sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) )
27 18 25 26 syl2anc 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) +e sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) + sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) )
28 15 5 6 sge0rern 
 |-  ( ph -> -. +oo e. ran F )
29 nelrnres 
 |-  ( -. +oo e. ran F -> -. +oo e. ran ( F |` A ) )
30 28 29 syl 
 |-  ( ph -> -. +oo e. ran ( F |` A ) )
31 11 30 fge0iccico 
 |-  ( ph -> ( F |` A ) : A --> ( 0 [,) +oo ) )
32 31 sge0rnre 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) C_ RR )
33 sge0rnn0 
 |-  ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) =/= (/)
34 33 a1i 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) =/= (/) )
35 1 31 sge0reval 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) = sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR* , < ) )
36 35 eqcomd 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR* , < ) = ( sum^ ` ( F |` A ) ) )
37 36 16 eqeltrd 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR* , < ) e. RR )
38 supxrre3 
 |-  ( ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) C_ RR /\ ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) =/= (/) ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR* , < ) e. RR <-> E. w e. RR A. t e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) t <_ w ) )
39 32 34 38 syl2anc 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR* , < ) e. RR <-> E. w e. RR A. t e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) t <_ w ) )
40 37 39 mpbid 
 |-  ( ph -> E. w e. RR A. t e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) t <_ w )
41 nelrnres 
 |-  ( -. +oo e. ran F -> -. +oo e. ran ( F |` B ) )
42 28 41 syl 
 |-  ( ph -> -. +oo e. ran ( F |` B ) )
43 22 42 fge0iccico 
 |-  ( ph -> ( F |` B ) : B --> ( 0 [,) +oo ) )
44 43 sge0rnre 
 |-  ( ph -> ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) C_ RR )
45 sge0rnn0 
 |-  ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) =/= (/)
46 45 a1i 
 |-  ( ph -> ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) =/= (/) )
47 2 43 sge0reval 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) = sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR* , < ) )
48 47 eqcomd 
 |-  ( ph -> sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR* , < ) = ( sum^ ` ( F |` B ) ) )
49 48 23 eqeltrd 
 |-  ( ph -> sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR* , < ) e. RR )
50 supxrre3 
 |-  ( ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) C_ RR /\ ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) =/= (/) ) -> ( sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR* , < ) e. RR <-> E. w e. RR A. t e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) t <_ w ) )
51 44 46 50 syl2anc 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR* , < ) e. RR <-> E. w e. RR A. t e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) t <_ w ) )
52 49 51 mpbid 
 |-  ( ph -> E. w e. RR A. t e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) t <_ w )
53 eqid 
 |-  { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } = { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) }
54 32 34 40 44 46 52 53 supadd 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) + sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) = sup ( { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } , RR , < ) )
55 simpl 
 |-  ( ( ph /\ r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } ) -> ph )
56 vex 
 |-  r e. _V
57 eqeq1 
 |-  ( z = r -> ( z = ( v + u ) <-> r = ( v + u ) ) )
58 57 rexbidv 
 |-  ( z = r -> ( E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) <-> E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) )
59 58 rexbidv 
 |-  ( z = r -> ( E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) <-> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) )
60 56 59 elab 
 |-  ( r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } <-> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) )
61 60 bilani 
 |-  ( ( ph /\ r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) )
62 simpl 
 |-  ( ( ph /\ ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) ) -> ph )
63 vex 
 |-  v e. _V
64 sumeq1 
 |-  ( x = a -> sum_ y e. x ( ( F |` A ) ` y ) = sum_ y e. a ( ( F |` A ) ` y ) )
65 64 cbvmptv 
 |-  ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) = ( a e. ( ~P A i^i Fin ) |-> sum_ y e. a ( ( F |` A ) ` y ) )
66 65 elrnmpt 
 |-  ( v e. _V -> ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) <-> E. a e. ( ~P A i^i Fin ) v = sum_ y e. a ( ( F |` A ) ` y ) ) )
67 63 66 ax-mp 
 |-  ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) <-> E. a e. ( ~P A i^i Fin ) v = sum_ y e. a ( ( F |` A ) ` y ) )
68 67 birani 
 |-  ( ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) -> E. a e. ( ~P A i^i Fin ) v = sum_ y e. a ( ( F |` A ) ` y ) )
69 vex 
 |-  u e. _V
70 sumeq1 
 |-  ( x = b -> sum_ y e. x ( ( F |` B ) ` y ) = sum_ y e. b ( ( F |` B ) ` y ) )
71 70 cbvmptv 
 |-  ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) = ( b e. ( ~P B i^i Fin ) |-> sum_ y e. b ( ( F |` B ) ` y ) )
72 71 elrnmpt 
 |-  ( u e. _V -> ( u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) <-> E. b e. ( ~P B i^i Fin ) u = sum_ y e. b ( ( F |` B ) ` y ) ) )
73 69 72 ax-mp 
 |-  ( u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) <-> E. b e. ( ~P B i^i Fin ) u = sum_ y e. b ( ( F |` B ) ` y ) )
74 73 bilani 
 |-  ( ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) -> E. b e. ( ~P B i^i Fin ) u = sum_ y e. b ( ( F |` B ) ` y ) )
75 68 74 jca 
 |-  ( ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) -> ( E. a e. ( ~P A i^i Fin ) v = sum_ y e. a ( ( F |` A ) ` y ) /\ E. b e. ( ~P B i^i Fin ) u = sum_ y e. b ( ( F |` B ) ` y ) ) )
76 reeanv 
 |-  ( E. a e. ( ~P A i^i Fin ) E. b e. ( ~P B i^i Fin ) ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) <-> ( E. a e. ( ~P A i^i Fin ) v = sum_ y e. a ( ( F |` A ) ` y ) /\ E. b e. ( ~P B i^i Fin ) u = sum_ y e. b ( ( F |` B ) ` y ) ) )
77 75 76 sylibr 
 |-  ( ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) -> E. a e. ( ~P A i^i Fin ) E. b e. ( ~P B i^i Fin ) ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) )
78 77 adantl 
 |-  ( ( ph /\ ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) ) -> E. a e. ( ~P A i^i Fin ) E. b e. ( ~P B i^i Fin ) ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) )
79 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 ) )
80 elinel1 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. ~P A )
81 elpwi 
 |-  ( a e. ~P A -> a C_ A )
82 id 
 |-  ( a C_ A -> a C_ A )
83 82 9 sstrdi 
 |-  ( a C_ A -> a C_ U )
84 81 83 syl 
 |-  ( a e. ~P A -> a C_ U )
85 80 84 syl 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ U )
86 85 adantr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> a C_ U )
87 elinel1 
 |-  ( b e. ( ~P B i^i Fin ) -> b e. ~P B )
88 elpwi 
 |-  ( b e. ~P B -> b C_ B )
89 id 
 |-  ( b C_ B -> b C_ B )
90 89 20 sstrdi 
 |-  ( b C_ B -> b C_ U )
91 88 90 syl 
 |-  ( b e. ~P B -> b C_ U )
92 87 91 syl 
 |-  ( b e. ( ~P B i^i Fin ) -> b C_ U )
93 92 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b C_ U )
94 86 93 unssd 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) C_ U )
95 vex 
 |-  a e. _V
96 vex 
 |-  b e. _V
97 95 96 unex 
 |-  ( a u. b ) e. _V
98 97 elpw 
 |-  ( ( a u. b ) e. ~P U <-> ( a u. b ) C_ U )
99 94 98 sylibr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. ~P U )
100 elinel2 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. Fin )
101 100 adantr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> a e. Fin )
102 elinel2 
 |-  ( b e. ( ~P B i^i Fin ) -> b e. Fin )
103 102 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b e. Fin )
104 unfi 
 |-  ( ( a e. Fin /\ b e. Fin ) -> ( a u. b ) e. Fin )
105 101 103 104 syl2anc 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. Fin )
106 99 105 elind 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. ( ~P U i^i Fin ) )
107 106 adantl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a u. b ) e. ( ~P U i^i Fin ) )
108 107 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> ( a u. b ) e. ( ~P U i^i Fin ) )
109 simpl 
 |-  ( ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> v = sum_ y e. a ( ( F |` A ) ` y ) )
110 simpr 
 |-  ( ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> u = sum_ y e. b ( ( F |` B ) ` y ) )
111 109 110 oveq12d 
 |-  ( ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> ( v + u ) = ( sum_ y e. a ( ( F |` A ) ` y ) + sum_ y e. b ( ( F |` B ) ` y ) ) )
112 111 adantl 
 |-  ( ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) -> ( v + u ) = ( sum_ y e. a ( ( F |` A ) ` y ) + sum_ y e. b ( ( F |` B ) ` y ) ) )
113 80 81 syl 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ A )
114 113 sselda 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ y e. a ) -> y e. A )
115 fvres 
 |-  ( y e. A -> ( ( F |` A ) ` y ) = ( F ` y ) )
116 114 115 syl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ y e. a ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
117 116 sumeq2dv 
 |-  ( a e. ( ~P A i^i Fin ) -> sum_ y e. a ( ( F |` A ) ` y ) = sum_ y e. a ( F ` y ) )
118 117 adantr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> sum_ y e. a ( ( F |` A ) ` y ) = sum_ y e. a ( F ` y ) )
119 87 88 syl 
 |-  ( b e. ( ~P B i^i Fin ) -> b C_ B )
120 119 sselda 
 |-  ( ( b e. ( ~P B i^i Fin ) /\ y e. b ) -> y e. B )
121 fvres 
 |-  ( y e. B -> ( ( F |` B ) ` y ) = ( F ` y ) )
122 120 121 syl 
 |-  ( ( b e. ( ~P B i^i Fin ) /\ y e. b ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
123 122 sumeq2dv 
 |-  ( b e. ( ~P B i^i Fin ) -> sum_ y e. b ( ( F |` B ) ` y ) = sum_ y e. b ( F ` y ) )
124 123 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> sum_ y e. b ( ( F |` B ) ` y ) = sum_ y e. b ( F ` y ) )
125 118 124 oveq12d 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( sum_ y e. a ( ( F |` A ) ` y ) + sum_ y e. b ( ( F |` B ) ` y ) ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
126 125 adantr 
 |-  ( ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) -> ( sum_ y e. a ( ( F |` A ) ` y ) + sum_ y e. b ( ( F |` B ) ` y ) ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
127 112 126 eqtrd 
 |-  ( ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) -> ( v + u ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
128 127 ad4ant23 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> ( v + u ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
129 simpr 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> r = ( v + u ) )
130 4 adantr 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( A i^i B ) = (/) )
131 113 ad2antrl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> a C_ A )
132 119 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b C_ B )
133 132 adantl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> b C_ B )
134 ssin0 
 |-  ( ( ( A i^i B ) = (/) /\ a C_ A /\ b C_ B ) -> ( a i^i b ) = (/) )
135 130 131 133 134 syl3anc 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a i^i b ) = (/) )
136 eqidd 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a u. b ) = ( a u. b ) )
137 105 adantl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a u. b ) e. Fin )
138 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
139 ax-resscn 
 |-  RR C_ CC
140 138 139 sstri 
 |-  ( 0 [,) +oo ) C_ CC
141 5 28 fge0iccico 
 |-  ( ph -> F : U --> ( 0 [,) +oo ) )
142 141 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ y e. ( a u. b ) ) -> F : U --> ( 0 [,) +oo ) )
143 94 sselda 
 |-  ( ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) /\ y e. ( a u. b ) ) -> y e. U )
144 143 adantll 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ y e. ( a u. b ) ) -> y e. U )
145 142 144 ffvelcdmd 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ y e. ( a u. b ) ) -> ( F ` y ) e. ( 0 [,) +oo ) )
146 140 145 sselid 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ y e. ( a u. b ) ) -> ( F ` y ) e. CC )
147 135 136 137 146 fsumsplit 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> sum_ y e. ( a u. b ) ( F ` y ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
148 147 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> sum_ y e. ( a u. b ) ( F ` y ) = ( sum_ y e. a ( F ` y ) + sum_ y e. b ( F ` y ) ) )
149 128 129 148 3eqtr4d 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> r = sum_ y e. ( a u. b ) ( F ` y ) )
150 sumeq1 
 |-  ( x = ( a u. b ) -> sum_ y e. x ( F ` y ) = sum_ y e. ( a u. b ) ( F ` y ) )
151 150 rspceeqv 
 |-  ( ( ( a u. b ) e. ( ~P U i^i Fin ) /\ r = sum_ y e. ( a u. b ) ( F ` y ) ) -> E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) )
152 108 149 151 syl2anc 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) )
153 56 a1i 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> r e. _V )
154 79 152 153 elrnmptd 
 |-  ( ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) /\ r = ( v + u ) ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
155 154 ex 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
156 155 ex 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) ) )
157 156 ex 
 |-  ( ph -> ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) ) ) )
158 157 rexlimdvv 
 |-  ( ph -> ( E. a e. ( ~P A i^i Fin ) E. b e. ( ~P B i^i Fin ) ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) ) )
159 158 imp 
 |-  ( ( ph /\ E. a e. ( ~P A i^i Fin ) E. b e. ( ~P B i^i Fin ) ( v = sum_ y e. a ( ( F |` A ) ` y ) /\ u = sum_ y e. b ( ( F |` B ) ` y ) ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
160 62 78 159 syl2anc 
 |-  ( ( ph /\ ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
161 160 ex 
 |-  ( ph -> ( ( v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) ) -> ( r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) ) )
162 161 rexlimdvv 
 |-  ( ph -> ( E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
163 162 imp 
 |-  ( ( ph /\ E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
164 55 61 163 syl2anc 
 |-  ( ( ph /\ r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } ) -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
165 164 ex 
 |-  ( ph -> ( r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } -> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
166 79 elrnmpt 
 |-  ( r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ( r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) ) )
167 166 ibi 
 |-  ( r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) )
168 167 adantl 
 |-  ( ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) )
169 nfv 
 |-  F/ x ph
170 nfcv 
 |-  F/_ x r
171 nfmpt1 
 |-  F/_ x ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
172 171 nfrn 
 |-  F/_ x ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
173 170 172 nfel 
 |-  F/ x r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
174 169 173 nfan 
 |-  F/ x ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
175 nfmpt1 
 |-  F/_ x ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) )
176 175 nfrn 
 |-  F/_ x ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) )
177 nfmpt1 
 |-  F/_ x ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) )
178 177 nfrn 
 |-  F/_ x ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) )
179 nfv 
 |-  F/ x r = ( v + u )
180 178 179 nfrexw 
 |-  F/ x E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u )
181 176 180 nfrexw 
 |-  F/ x E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u )
182 inss2 
 |-  ( x i^i A ) C_ A
183 182 sseli 
 |-  ( y e. ( x i^i A ) -> y e. A )
184 183 adantl 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. ( x i^i A ) ) -> y e. A )
185 115 eqcomd 
 |-  ( y e. A -> ( F ` y ) = ( ( F |` A ) ` y ) )
186 184 185 syl 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. ( x i^i A ) ) -> ( F ` y ) = ( ( F |` A ) ` y ) )
187 186 sumeq2dv 
 |-  ( x e. ( ~P U i^i Fin ) -> sum_ y e. ( x i^i A ) ( F ` y ) = sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) )
188 sumeq1 
 |-  ( x = z -> sum_ y e. x ( ( F |` A ) ` y ) = sum_ y e. z ( ( F |` A ) ` y ) )
189 188 cbvmptv 
 |-  ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) = ( z e. ( ~P A i^i Fin ) |-> sum_ y e. z ( ( F |` A ) ` y ) )
190 vex 
 |-  x e. _V
191 190 inex1 
 |-  ( x i^i A ) e. _V
192 191 elpw 
 |-  ( ( x i^i A ) e. ~P A <-> ( x i^i A ) C_ A )
193 182 192 mpbir 
 |-  ( x i^i A ) e. ~P A
194 193 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. ~P A )
195 elinel2 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. Fin )
196 inss1 
 |-  ( x i^i A ) C_ x
197 196 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) C_ x )
198 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i A ) C_ x ) -> ( x i^i A ) e. Fin )
199 195 197 198 syl2anc 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. Fin )
200 194 199 elind 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. ( ~P A i^i Fin ) )
201 eqidd 
 |-  ( 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 |` A ) ` y ) )
202 sumeq1 
 |-  ( z = ( x i^i A ) -> sum_ y e. z ( ( F |` A ) ` y ) = sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) )
203 202 rspceeqv 
 |-  ( ( ( x i^i A ) e. ( ~P A i^i Fin ) /\ sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) = sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) ) -> E. z e. ( ~P A i^i Fin ) sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) = sum_ y e. z ( ( F |` A ) ` y ) )
204 200 201 203 syl2anc 
 |-  ( x e. ( ~P U i^i Fin ) -> E. z e. ( ~P A i^i Fin ) sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) = sum_ y e. z ( ( F |` A ) ` y ) )
205 sumex 
 |-  sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) e. _V
206 205 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) e. _V )
207 189 204 206 elrnmptd 
 |-  ( x e. ( ~P U i^i Fin ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) )
208 187 207 eqeltrd 
 |-  ( x e. ( ~P U i^i Fin ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) )
209 208 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) )
210 sumeq1 
 |-  ( x = z -> sum_ y e. x ( ( F |` B ) ` y ) = sum_ y e. z ( ( F |` B ) ` y ) )
211 210 cbvmptv 
 |-  ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) = ( z e. ( ~P B i^i Fin ) |-> sum_ y e. z ( ( F |` B ) ` y ) )
212 inss2 
 |-  ( x i^i B ) C_ B
213 190 inex1 
 |-  ( x i^i B ) e. _V
214 213 elpw 
 |-  ( ( x i^i B ) e. ~P B <-> ( x i^i B ) C_ B )
215 212 214 mpbir 
 |-  ( x i^i B ) e. ~P B
216 215 a1i 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> ( x i^i B ) e. ~P B )
217 inss1 
 |-  ( x i^i B ) C_ x
218 217 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) C_ x )
219 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i B ) C_ x ) -> ( x i^i B ) e. Fin )
220 195 218 219 syl2anc 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) e. Fin )
221 220 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> ( x i^i B ) e. Fin )
222 216 221 elind 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> ( x i^i B ) e. ( ~P B i^i Fin ) )
223 212 sseli 
 |-  ( y e. ( x i^i B ) -> y e. B )
224 121 eqcomd 
 |-  ( y e. B -> ( F ` y ) = ( ( F |` B ) ` y ) )
225 223 224 syl 
 |-  ( y e. ( x i^i B ) -> ( F ` y ) = ( ( F |` B ) ` y ) )
226 225 sumeq2i 
 |-  sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y )
227 226 a1i 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) )
228 227 3adant3 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) )
229 sumeq1 
 |-  ( z = ( x i^i B ) -> sum_ y e. z ( ( F |` B ) ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) )
230 229 rspceeqv 
 |-  ( ( ( x i^i B ) e. ( ~P B i^i Fin ) /\ sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) ) -> E. z e. ( ~P B i^i Fin ) sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. z ( ( F |` B ) ` y ) )
231 222 228 230 syl2anc 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> E. z e. ( ~P B i^i Fin ) sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. z ( ( F |` B ) ` y ) )
232 sumex 
 |-  sum_ y e. ( x i^i B ) ( F ` y ) e. _V
233 232 a1i 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. _V )
234 211 231 233 elrnmptd 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) )
235 simp3 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> r = sum_ y e. x ( F ` y ) )
236 182 a1i 
 |-  ( ph -> ( x i^i A ) C_ A )
237 212 a1i 
 |-  ( ph -> ( x i^i B ) C_ B )
238 ssin0 
 |-  ( ( ( A i^i B ) = (/) /\ ( x i^i A ) C_ A /\ ( x i^i B ) C_ B ) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
239 4 236 237 238 syl3anc 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
240 239 adantr 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
241 elinel1 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. ~P U )
242 elpwi 
 |-  ( x e. ~P U -> x C_ U )
243 241 242 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x C_ U )
244 3 ineq2i 
 |-  ( x i^i U ) = ( x i^i ( A u. B ) )
245 244 a1i 
 |-  ( x C_ U -> ( x i^i U ) = ( x i^i ( A u. B ) ) )
246 dfss 
 |-  ( x C_ U <-> x = ( x i^i U ) )
247 246 biimpi 
 |-  ( x C_ U -> x = ( x i^i U ) )
248 indi 
 |-  ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( x i^i B ) )
249 248 eqcomi 
 |-  ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) )
250 249 a1i 
 |-  ( x C_ U -> ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) ) )
251 245 247 250 3eqtr4d 
 |-  ( x C_ U -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
252 243 251 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
253 252 adantl 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
254 195 adantl 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> x e. Fin )
255 141 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> F : U --> ( 0 [,) +oo ) )
256 243 sselda 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. U )
257 256 adantll 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> y e. U )
258 255 257 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
259 140 258 sselid 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. CC )
260 240 253 254 259 fsumsplit 
 |-  ( ( ph /\ 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 ) ) )
261 260 3adant3 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> sum_ y e. x ( F ` y ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
262 235 261 eqtrd 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> r = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
263 oveq2 
 |-  ( u = sum_ y e. ( x i^i B ) ( F ` y ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
264 263 rspceeqv 
 |-  ( ( sum_ y e. ( x i^i B ) ( F ` y ) e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) /\ r = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) ) -> E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) )
265 234 262 264 syl2anc 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) )
266 oveq1 
 |-  ( v = sum_ y e. ( x i^i A ) ( F ` y ) -> ( v + u ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) )
267 266 eqeq2d 
 |-  ( v = sum_ y e. ( x i^i A ) ( F ` y ) -> ( r = ( v + u ) <-> r = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) ) )
268 267 rexbidv 
 |-  ( v = sum_ y e. ( x i^i A ) ( F ` y ) -> ( E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) <-> E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) ) )
269 268 rspcev 
 |-  ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) /\ E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) )
270 209 265 269 syl2anc 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) )
271 270 3exp 
 |-  ( ph -> ( x e. ( ~P U i^i Fin ) -> ( r = sum_ y e. x ( F ` y ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) ) )
272 271 adantr 
 |-  ( ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( x e. ( ~P U i^i Fin ) -> ( r = sum_ y e. x ( F ` y ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) ) )
273 174 181 272 rexlimd 
 |-  ( ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( E. x e. ( ~P U i^i Fin ) r = sum_ y e. x ( F ` y ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) ) )
274 168 273 mpd 
 |-  ( ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u ) )
275 274 60 sylibr 
 |-  ( ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } )
276 275 ex 
 |-  ( ph -> ( r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } ) )
277 165 276 impbid 
 |-  ( ph -> ( r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } <-> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
278 277 alrimiv 
 |-  ( ph -> A. r ( r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } <-> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
279 dfcleq 
 |-  ( { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } = ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> A. r ( r e. { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } <-> r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) )
280 278 279 sylibr 
 |-  ( ph -> { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } = ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
281 280 supeq1d 
 |-  ( ph -> sup ( { z | E. v e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) z = ( v + u ) } , RR , < ) = sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
282 27 54 281 3eqtrrd 
 |-  ( ph -> sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) +e sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) )
283 15 5 6 sge0supre 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
284 17 24 oveq12d 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) ) , RR , < ) +e sup ( ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) , RR , < ) ) )
285 282 283 284 3eqtr4d 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
286 rexadd 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR /\ ( sum^ ` ( F |` B ) ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
287 16 23 286 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
288 285 287 eqtrd 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )