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 biimpi 
 |-  ( 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 61 adantl 
 |-  ( ( 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 ) )
63 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 )
64 vex 
 |-  v e. _V
65 sumeq1 
 |-  ( x = a -> sum_ y e. x ( ( F |` A ) ` y ) = sum_ y e. a ( ( F |` A ) ` y ) )
66 65 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 ) )
67 66 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 ) ) )
68 64 67 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 ) )
69 68 biimpi 
 |-  ( 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 ) )
70 69 adantr 
 |-  ( ( 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 ) )
71 vex 
 |-  u e. _V
72 sumeq1 
 |-  ( x = b -> sum_ y e. x ( ( F |` B ) ` y ) = sum_ y e. b ( ( F |` B ) ` y ) )
73 72 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 ) )
74 73 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 ) ) )
75 71 74 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 ) )
76 75 biimpi 
 |-  ( 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 ) )
77 76 adantl 
 |-  ( ( 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 ) )
78 70 77 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 ) ) )
79 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 ) ) )
80 78 79 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 ) ) )
81 80 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 ) ) )
82 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 ) )
83 elinel1 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. ~P A )
84 elpwi 
 |-  ( a e. ~P A -> a C_ A )
85 id 
 |-  ( a C_ A -> a C_ A )
86 85 9 sstrdi 
 |-  ( a C_ A -> a C_ U )
87 84 86 syl 
 |-  ( a e. ~P A -> a C_ U )
88 83 87 syl 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ U )
89 88 adantr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> a C_ U )
90 elinel1 
 |-  ( b e. ( ~P B i^i Fin ) -> b e. ~P B )
91 elpwi 
 |-  ( b e. ~P B -> b C_ B )
92 id 
 |-  ( b C_ B -> b C_ B )
93 92 20 sstrdi 
 |-  ( b C_ B -> b C_ U )
94 91 93 syl 
 |-  ( b e. ~P B -> b C_ U )
95 90 94 syl 
 |-  ( b e. ( ~P B i^i Fin ) -> b C_ U )
96 95 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b C_ U )
97 89 96 unssd 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) C_ U )
98 vex 
 |-  a e. _V
99 vex 
 |-  b e. _V
100 98 99 unex 
 |-  ( a u. b ) e. _V
101 100 elpw 
 |-  ( ( a u. b ) e. ~P U <-> ( a u. b ) C_ U )
102 97 101 sylibr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. ~P U )
103 elinel2 
 |-  ( a e. ( ~P A i^i Fin ) -> a e. Fin )
104 103 adantr 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> a e. Fin )
105 elinel2 
 |-  ( b e. ( ~P B i^i Fin ) -> b e. Fin )
106 105 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b e. Fin )
107 unfi 
 |-  ( ( a e. Fin /\ b e. Fin ) -> ( a u. b ) e. Fin )
108 104 106 107 syl2anc 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. Fin )
109 102 108 elind 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> ( a u. b ) e. ( ~P U i^i Fin ) )
110 109 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 ) )
111 110 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 ) )
112 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 ) )
113 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 ) )
114 112 113 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 ) ) )
115 114 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 ) ) )
116 83 84 syl 
 |-  ( a e. ( ~P A i^i Fin ) -> a C_ A )
117 116 sselda 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ y e. a ) -> y e. A )
118 fvres 
 |-  ( y e. A -> ( ( F |` A ) ` y ) = ( F ` y ) )
119 117 118 syl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ y e. a ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
120 119 sumeq2dv 
 |-  ( a e. ( ~P A i^i Fin ) -> sum_ y e. a ( ( F |` A ) ` y ) = sum_ y e. a ( F ` y ) )
121 120 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 ) )
122 90 91 syl 
 |-  ( b e. ( ~P B i^i Fin ) -> b C_ B )
123 122 sselda 
 |-  ( ( b e. ( ~P B i^i Fin ) /\ y e. b ) -> y e. B )
124 fvres 
 |-  ( y e. B -> ( ( F |` B ) ` y ) = ( F ` y ) )
125 123 124 syl 
 |-  ( ( b e. ( ~P B i^i Fin ) /\ y e. b ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
126 125 sumeq2dv 
 |-  ( b e. ( ~P B i^i Fin ) -> sum_ y e. b ( ( F |` B ) ` y ) = sum_ y e. b ( F ` y ) )
127 126 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 ) )
128 121 127 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 ) ) )
129 128 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 ) ) )
130 115 129 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 ) ) )
131 130 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 ) ) )
132 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 ) )
133 4 adantr 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( A i^i B ) = (/) )
134 116 ad2antrl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> a C_ A )
135 122 adantl 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) -> b C_ B )
136 135 adantl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> b C_ B )
137 ssin0 
 |-  ( ( ( A i^i B ) = (/) /\ a C_ A /\ b C_ B ) -> ( a i^i b ) = (/) )
138 133 134 136 137 syl3anc 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a i^i b ) = (/) )
139 eqidd 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a u. b ) = ( a u. b ) )
140 108 adantl 
 |-  ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) -> ( a u. b ) e. Fin )
141 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
142 ax-resscn 
 |-  RR C_ CC
143 141 142 sstri 
 |-  ( 0 [,) +oo ) C_ CC
144 5 28 fge0iccico 
 |-  ( ph -> F : U --> ( 0 [,) +oo ) )
145 144 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 ) )
146 97 sselda 
 |-  ( ( ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) /\ y e. ( a u. b ) ) -> y e. U )
147 146 adantll 
 |-  ( ( ( ph /\ ( a e. ( ~P A i^i Fin ) /\ b e. ( ~P B i^i Fin ) ) ) /\ y e. ( a u. b ) ) -> y e. U )
148 145 147 ffvelrnd 
 |-  ( ( ( 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 ) )
149 143 148 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 )
150 138 139 140 149 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 ) ) )
151 150 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 ) ) )
152 131 132 151 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 ) )
153 sumeq1 
 |-  ( x = ( a u. b ) -> sum_ y e. x ( F ` y ) = sum_ y e. ( a u. b ) ( F ` y ) )
154 153 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 ) )
155 111 152 154 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 ) )
156 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 )
157 82 155 156 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 ) ) )
158 157 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 ) ) ) )
159 158 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 ) ) ) ) )
160 159 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 ) ) ) ) ) )
161 160 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 ) ) ) ) )
162 161 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 ) ) ) )
163 63 81 162 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 ) ) ) )
164 163 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 ) ) ) ) )
165 164 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 ) ) ) )
166 165 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 ) ) )
167 55 62 166 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 ) ) )
168 167 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 ) ) ) )
169 82 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 ) ) )
170 169 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 ) )
171 170 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 ) )
172 nfv 
 |-  F/ x ph
173 nfcv 
 |-  F/_ x r
174 nfmpt1 
 |-  F/_ x ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
175 174 nfrn 
 |-  F/_ x ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
176 173 175 nfel 
 |-  F/ x r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
177 172 176 nfan 
 |-  F/ x ( ph /\ r e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
178 nfmpt1 
 |-  F/_ x ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) )
179 178 nfrn 
 |-  F/_ x ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( F |` A ) ` y ) )
180 nfmpt1 
 |-  F/_ x ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) )
181 180 nfrn 
 |-  F/_ x ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) )
182 nfv 
 |-  F/ x r = ( v + u )
183 181 182 nfrex 
 |-  F/ x E. u e. ran ( x e. ( ~P B i^i Fin ) |-> sum_ y e. x ( ( F |` B ) ` y ) ) r = ( v + u )
184 179 183 nfrex 
 |-  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 )
185 inss2 
 |-  ( x i^i A ) C_ A
186 185 sseli 
 |-  ( y e. ( x i^i A ) -> y e. A )
187 186 adantl 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. ( x i^i A ) ) -> y e. A )
188 118 eqcomd 
 |-  ( y e. A -> ( F ` y ) = ( ( F |` A ) ` y ) )
189 187 188 syl 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. ( x i^i A ) ) -> ( F ` y ) = ( ( F |` A ) ` y ) )
190 189 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 ) )
191 sumeq1 
 |-  ( x = z -> sum_ y e. x ( ( F |` A ) ` y ) = sum_ y e. z ( ( F |` A ) ` y ) )
192 191 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 ) )
193 vex 
 |-  x e. _V
194 193 inex1 
 |-  ( x i^i A ) e. _V
195 194 elpw 
 |-  ( ( x i^i A ) e. ~P A <-> ( x i^i A ) C_ A )
196 185 195 mpbir 
 |-  ( x i^i A ) e. ~P A
197 196 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. ~P A )
198 elinel2 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. Fin )
199 inss1 
 |-  ( x i^i A ) C_ x
200 199 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) C_ x )
201 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i A ) C_ x ) -> ( x i^i A ) e. Fin )
202 198 200 201 syl2anc 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. Fin )
203 197 202 elind 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. ( ~P A i^i Fin ) )
204 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 ) )
205 sumeq1 
 |-  ( z = ( x i^i A ) -> sum_ y e. z ( ( F |` A ) ` y ) = sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) )
206 205 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 ) )
207 203 204 206 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 ) )
208 sumex 
 |-  sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) e. _V
209 208 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) e. _V )
210 192 207 209 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 ) ) )
211 190 210 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 ) ) )
212 211 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 ) ) )
213 sumeq1 
 |-  ( x = z -> sum_ y e. x ( ( F |` B ) ` y ) = sum_ y e. z ( ( F |` B ) ` y ) )
214 213 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 ) )
215 inss2 
 |-  ( x i^i B ) C_ B
216 193 inex1 
 |-  ( x i^i B ) e. _V
217 216 elpw 
 |-  ( ( x i^i B ) e. ~P B <-> ( x i^i B ) C_ B )
218 215 217 mpbir 
 |-  ( x i^i B ) e. ~P B
219 218 a1i 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> ( x i^i B ) e. ~P B )
220 inss1 
 |-  ( x i^i B ) C_ x
221 220 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) C_ x )
222 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i B ) C_ x ) -> ( x i^i B ) e. Fin )
223 198 221 222 syl2anc 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) e. Fin )
224 223 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> ( x i^i B ) e. Fin )
225 219 224 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 ) )
226 215 sseli 
 |-  ( y e. ( x i^i B ) -> y e. B )
227 124 eqcomd 
 |-  ( y e. B -> ( F ` y ) = ( ( F |` B ) ` y ) )
228 226 227 syl 
 |-  ( y e. ( x i^i B ) -> ( F ` y ) = ( ( F |` B ) ` y ) )
229 228 sumeq2i 
 |-  sum_ y e. ( x i^i B ) ( F ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y )
230 229 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 ) )
231 230 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 ) )
232 sumeq1 
 |-  ( z = ( x i^i B ) -> sum_ y e. z ( ( F |` B ) ` y ) = sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) )
233 232 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 ) )
234 225 231 233 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 ) )
235 sumex 
 |-  sum_ y e. ( x i^i B ) ( F ` y ) e. _V
236 235 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 )
237 214 234 236 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 ) ) )
238 simp3 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) /\ r = sum_ y e. x ( F ` y ) ) -> r = sum_ y e. x ( F ` y ) )
239 185 a1i 
 |-  ( ph -> ( x i^i A ) C_ A )
240 215 a1i 
 |-  ( ph -> ( x i^i B ) C_ B )
241 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 ) ) = (/) )
242 4 239 240 241 syl3anc 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
243 242 adantr 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
244 elinel1 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. ~P U )
245 elpwi 
 |-  ( x e. ~P U -> x C_ U )
246 244 245 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x C_ U )
247 3 ineq2i 
 |-  ( x i^i U ) = ( x i^i ( A u. B ) )
248 247 a1i 
 |-  ( x C_ U -> ( x i^i U ) = ( x i^i ( A u. B ) ) )
249 dfss 
 |-  ( x C_ U <-> x = ( x i^i U ) )
250 249 biimpi 
 |-  ( x C_ U -> x = ( x i^i U ) )
251 indi 
 |-  ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( x i^i B ) )
252 251 eqcomi 
 |-  ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) )
253 252 a1i 
 |-  ( x C_ U -> ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) ) )
254 248 250 253 3eqtr4d 
 |-  ( x C_ U -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
255 246 254 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
256 255 adantl 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
257 198 adantl 
 |-  ( ( ph /\ x e. ( ~P U i^i Fin ) ) -> x e. Fin )
258 144 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> F : U --> ( 0 [,) +oo ) )
259 246 sselda 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. U )
260 259 adantll 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> y e. U )
261 258 260 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
262 143 261 sselid 
 |-  ( ( ( ph /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. CC )
263 243 256 257 262 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 ) ) )
264 263 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 ) ) )
265 238 264 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 ) ) )
266 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 ) ) )
267 266 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 ) )
268 237 265 267 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 ) )
269 oveq1 
 |-  ( v = sum_ y e. ( x i^i A ) ( F ` y ) -> ( v + u ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + u ) )
270 269 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 ) ) )
271 270 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 ) ) )
272 271 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 ) )
273 212 268 272 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 ) )
274 273 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 ) ) ) )
275 274 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 ) ) ) )
276 177 184 275 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 ) ) )
277 171 276 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 ) )
278 277 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 ) } )
279 278 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 ) } ) )
280 168 279 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 ) ) ) )
281 280 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 ) ) ) )
282 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 ) ) ) )
283 281 282 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 ) ) )
284 283 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 , < ) )
285 27 54 284 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 , < ) ) )
286 15 5 6 sge0supre 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
287 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 , < ) ) )
288 285 286 287 3eqtr4d 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
289 rexadd 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR /\ ( sum^ ` ( F |` B ) ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
290 16 23 289 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
291 288 290 eqtrd 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )