Step |
Hyp |
Ref |
Expression |
1 |
|
esumadd.0 |
|- ( ph -> A e. V ) |
2 |
|
esumadd.1 |
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) ) |
3 |
|
esumadd.2 |
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) ) |
4 |
|
nfv |
|- F/ k ph |
5 |
|
nfcv |
|- F/_ k A |
6 |
|
ge0xaddcl |
|- ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B +e C ) e. ( 0 [,] +oo ) ) |
7 |
2 3 6
|
syl2anc |
|- ( ( ph /\ k e. A ) -> ( B +e C ) e. ( 0 [,] +oo ) ) |
8 |
|
xrge0base |
|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
9 |
|
xrge0plusg |
|- +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
10 |
|
xrge0cmn |
|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd |
11 |
10
|
a1i |
|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd ) |
12 |
|
xrge0tmd |
|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd |
13 |
12
|
a1i |
|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd ) |
14 |
2
|
fmpttd |
|- ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) ) |
15 |
3
|
fmpttd |
|- ( ph -> ( k e. A |-> C ) : A --> ( 0 [,] +oo ) ) |
16 |
4 5 1 2
|
esumel |
|- ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) ) |
17 |
4 5 1 3
|
esumel |
|- ( ph -> sum* k e. A C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) ) |
18 |
8 9 11 13 1 14 15 16 17
|
tsmsadd |
|- ( ph -> ( sum* k e. A B +e sum* k e. A C ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) ) ) |
19 |
|
eqidd |
|- ( ph -> ( k e. A |-> B ) = ( k e. A |-> B ) ) |
20 |
|
eqidd |
|- ( ph -> ( k e. A |-> C ) = ( k e. A |-> C ) ) |
21 |
1 2 3 19 20
|
offval2 |
|- ( ph -> ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) = ( k e. A |-> ( B +e C ) ) ) |
22 |
21
|
oveq2d |
|- ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( B +e C ) ) ) ) |
23 |
18 22
|
eleqtrd |
|- ( ph -> ( sum* k e. A B +e sum* k e. A C ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( B +e C ) ) ) ) |
24 |
4 5 1 7 23
|
esumid |
|- ( ph -> sum* k e. A ( B +e C ) = ( sum* k e. A B +e sum* k e. A C ) ) |