Metamath Proof Explorer

Theorem sge0xadd

Description: The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0xadd.kph 
|- F/ k ph
sge0xadd.a 
|- ( ph -> A e. V )
sge0xadd.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
sge0xadd.c 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
Assertion sge0xadd 
|- ( ph -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0xadd.kph 
 |-  F/ k ph
2 sge0xadd.a 
 |-  ( ph -> A e. V )
3 sge0xadd.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4 sge0xadd.c 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
5 simpr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> B ) ) = +oo )
6 5 oveq1d 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) = ( +oo +e ( sum^ ` ( k e. A |-> C ) ) ) )
7 1 2 4 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) e. RR* )
8 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
9 1 4 8 fmptdf 
 |-  ( ph -> ( k e. A |-> C ) : A --> ( 0 [,] +oo ) )
10 2 9 sge0nemnf 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) =/= -oo )
11 xaddpnf2 
 |-  ( ( ( sum^ ` ( k e. A |-> C ) ) e. RR* /\ ( sum^ ` ( k e. A |-> C ) ) =/= -oo ) -> ( +oo +e ( sum^ ` ( k e. A |-> C ) ) ) = +oo )
12 7 10 11 syl2anc 
 |-  ( ph -> ( +oo +e ( sum^ ` ( k e. A |-> C ) ) ) = +oo )
13 12 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( +oo +e ( sum^ ` ( k e. A |-> C ) ) ) = +oo )
14 ge0xaddcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B +e C ) e. ( 0 [,] +oo ) )
15 3 4 14 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( B +e C ) e. ( 0 [,] +oo ) )
16 1 2 15 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) e. RR* )
17 16 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) e. RR* )
18 id 
 |-  ( ( sum^ ` ( k e. A |-> B ) ) = +oo -> ( sum^ ` ( k e. A |-> B ) ) = +oo )
19 18 eqcomd 
 |-  ( ( sum^ ` ( k e. A |-> B ) ) = +oo -> +oo = ( sum^ ` ( k e. A |-> B ) ) )
20 19 adantl 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> +oo = ( sum^ ` ( k e. A |-> B ) ) )
21 2 elexd 
 |-  ( ph -> A e. _V )
22 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
23 22 3 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. RR* )
24 23 4 xadd0ge 
 |-  ( ( ph /\ k e. A ) -> B <_ ( B +e C ) )
25 1 21 3 15 24 sge0lempt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
26 25 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> B ) ) <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
27 20 26 eqbrtrd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> +oo <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
28 17 27 xrgepnfd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = +oo )
29 28 eqcomd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> +oo = ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
30 6 13 29 3eqtrrd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
31 simpl 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ph )
32 simpr 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> -. ( sum^ ` ( k e. A |-> B ) ) = +oo )
33 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
34 1 3 33 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
35 2 34 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) )
36 35 adantr 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( ( sum^ ` ( k e. A |-> B ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) )
37 32 36 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
38 simpr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> C ) ) = +oo )
39 38 oveq2d 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e +oo ) )
40 2 34 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) e. RR* )
41 2 34 sge0nemnf 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) =/= -oo )
42 xaddpnf1 
 |-  ( ( ( sum^ ` ( k e. A |-> B ) ) e. RR* /\ ( sum^ ` ( k e. A |-> B ) ) =/= -oo ) -> ( ( sum^ ` ( k e. A |-> B ) ) +e +oo ) = +oo )
43 40 41 42 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) +e +oo ) = +oo )
44 43 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( ( sum^ ` ( k e. A |-> B ) ) +e +oo ) = +oo )
45 16 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) e. RR* )
46 id 
 |-  ( ( sum^ ` ( k e. A |-> C ) ) = +oo -> ( sum^ ` ( k e. A |-> C ) ) = +oo )
47 46 eqcomd 
 |-  ( ( sum^ ` ( k e. A |-> C ) ) = +oo -> +oo = ( sum^ ` ( k e. A |-> C ) ) )
48 47 adantl 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> +oo = ( sum^ ` ( k e. A |-> C ) ) )
49 22 4 sselid 
 |-  ( ( ph /\ k e. A ) -> C e. RR* )
50 49 3 xadd0ge2 
 |-  ( ( ph /\ k e. A ) -> C <_ ( B +e C ) )
51 1 2 4 15 50 sge0lempt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
52 51 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> C ) ) <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
53 48 52 eqbrtrd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> +oo <_ ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
54 45 53 xrgepnfd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = +oo )
55 54 eqcomd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> +oo = ( sum^ ` ( k e. A |-> ( B +e C ) ) ) )
56 39 44 55 3eqtrrd 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
57 56 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
58 simpl 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) )
59 simpr 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> -. ( sum^ ` ( k e. A |-> C ) ) = +oo )
60 2 9 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> C ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) )
61 60 adantr 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( ( sum^ ` ( k e. A |-> C ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) )
62 59 61 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
63 62 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
64 2 ad2antrr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> A e. V )
65 nfcv 
 |-  F/_ k sum^
66 nfmpt1 
 |-  F/_ k ( k e. A |-> B )
67 65 66 nffv 
 |-  F/_ k ( sum^ ` ( k e. A |-> B ) )
68 nfcv 
 |-  F/_ k RR
69 67 68 nfel 
 |-  F/ k ( sum^ ` ( k e. A |-> B ) ) e. RR
70 1 69 nfan 
 |-  F/ k ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR )
71 nfv 
 |-  F/ k j e. A
72 70 71 nfan 
 |-  F/ k ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ j e. A )
73 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
74 73 nfel1 
 |-  F/ k [_ j / k ]_ B e. ( 0 [,) +oo )
75 72 74 nfim 
 |-  F/ k ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ B e. ( 0 [,) +oo ) )
76 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
77 76 anbi2d 
 |-  ( k = j -> ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ k e. A ) <-> ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ j e. A ) ) )
78 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
79 78 eleq1d 
 |-  ( k = j -> ( B e. ( 0 [,) +oo ) <-> [_ j / k ]_ B e. ( 0 [,) +oo ) ) )
80 77 79 imbi12d 
 |-  ( k = j -> ( ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ k e. A ) -> B e. ( 0 [,) +oo ) ) <-> ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ B e. ( 0 [,) +oo ) ) ) )
81 2 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) -> A e. V )
82 3 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ k e. A ) -> B e. ( 0 [,] +oo ) )
83 simpr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
84 70 81 82 83 sge0rernmpt 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ k e. A ) -> B e. ( 0 [,) +oo ) )
85 75 80 84 chvarfv 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ B e. ( 0 [,) +oo ) )
86 85 adantlr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ B e. ( 0 [,) +oo ) )
87 nfmpt1 
 |-  F/_ k ( k e. A |-> C )
88 65 87 nffv 
 |-  F/_ k ( sum^ ` ( k e. A |-> C ) )
89 88 68 nfel 
 |-  F/ k ( sum^ ` ( k e. A |-> C ) ) e. RR
90 1 89 nfan 
 |-  F/ k ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR )
91 90 71 nfan 
 |-  F/ k ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A )
92 nfcsb1v 
 |-  F/_ k [_ j / k ]_ C
93 92 nfel1 
 |-  F/ k [_ j / k ]_ C e. ( 0 [,) +oo )
94 91 93 nfim 
 |-  F/ k ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ C e. ( 0 [,) +oo ) )
95 76 anbi2d 
 |-  ( k = j -> ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ k e. A ) <-> ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) ) )
96 csbeq1a 
 |-  ( k = j -> C = [_ j / k ]_ C )
97 96 eleq1d 
 |-  ( k = j -> ( C e. ( 0 [,) +oo ) <-> [_ j / k ]_ C e. ( 0 [,) +oo ) ) )
98 95 97 imbi12d 
 |-  ( k = j -> ( ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ k e. A ) -> C e. ( 0 [,) +oo ) ) <-> ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ C e. ( 0 [,) +oo ) ) ) )
99 2 adantr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> A e. V )
100 4 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ k e. A ) -> C e. ( 0 [,] +oo ) )
101 simpr 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
102 90 99 100 101 sge0rernmpt 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ k e. A ) -> C e. ( 0 [,) +oo ) )
103 94 98 102 chvarfv 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ C e. ( 0 [,) +oo ) )
104 103 adantllr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) /\ j e. A ) -> [_ j / k ]_ C e. ( 0 [,) +oo ) )
105 nfcv 
 |-  F/_ j B
106 105 73 78 cbvmpt 
 |-  ( k e. A |-> B ) = ( j e. A |-> [_ j / k ]_ B )
107 106 fveq2i 
 |-  ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) )
108 simplr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
109 107 108 eqeltrrid 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) ) e. RR )
110 nfcv 
 |-  F/_ j C
111 110 92 96 cbvmpt 
 |-  ( k e. A |-> C ) = ( j e. A |-> [_ j / k ]_ C )
112 111 fveq2i 
 |-  ( sum^ ` ( k e. A |-> C ) ) = ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) )
113 simpr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
114 112 113 eqeltrrid 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) ) e. RR )
115 64 86 104 109 114 sge0xaddlem2 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( j e. A |-> ( [_ j / k ]_ B +e [_ j / k ]_ C ) ) ) = ( ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) ) +e ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) ) ) )
116 nfcv 
 |-  F/_ j ( B +e C )
117 nfcv 
 |-  F/_ k +e
118 73 117 92 nfov 
 |-  F/_ k ( [_ j / k ]_ B +e [_ j / k ]_ C )
119 78 96 oveq12d 
 |-  ( k = j -> ( B +e C ) = ( [_ j / k ]_ B +e [_ j / k ]_ C ) )
120 116 118 119 cbvmpt 
 |-  ( k e. A |-> ( B +e C ) ) = ( j e. A |-> ( [_ j / k ]_ B +e [_ j / k ]_ C ) )
121 120 fveq2i 
 |-  ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( sum^ ` ( j e. A |-> ( [_ j / k ]_ B +e [_ j / k ]_ C ) ) )
122 107 112 oveq12i 
 |-  ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) = ( ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) ) +e ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) ) )
123 121 122 eqeq12i 
 |-  ( ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) <-> ( sum^ ` ( j e. A |-> ( [_ j / k ]_ B +e [_ j / k ]_ C ) ) ) = ( ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) ) +e ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) ) ) )
124 115 123 sylibr 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ ( sum^ ` ( k e. A |-> C ) ) e. RR ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
125 58 63 124 syl2anc 
 |-  ( ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) /\ -. ( sum^ ` ( k e. A |-> C ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
126 57 125 pm2.61dan 
 |-  ( ( ph /\ ( sum^ ` ( k e. A |-> B ) ) e. RR ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
127 31 37 126 syl2anc 
 |-  ( ( ph /\ -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )
128 30 127 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )