Metamath Proof Explorer


Theorem sge0ss

Description: Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ss.kph k φ
sge0ss.b φ B V
sge0ss.a φ A B
sge0ss.c φ k A C 0 +∞
sge0ss.c0 φ k B A C = 0
Assertion sge0ss φ sum^ k A C = sum^ k B C

Proof

Step Hyp Ref Expression
1 sge0ss.kph k φ
2 sge0ss.b φ B V
3 sge0ss.a φ A B
4 sge0ss.c φ k A C 0 +∞
5 sge0ss.c0 φ k B A C = 0
6 ssexg A B B V A V
7 3 2 6 syl2anc φ A V
8 2 difexd φ B A V
9 disjdif A B A =
10 9 a1i φ A B A =
11 0e0iccpnf 0 0 +∞
12 11 a1i φ k B A 0 0 +∞
13 5 12 eqeltrd φ k B A C 0 +∞
14 1 7 8 10 4 13 sge0splitmpt φ sum^ k A B A C = sum^ k A C + 𝑒 sum^ k B A C
15 14 eqcomd φ sum^ k A C + 𝑒 sum^ k B A C = sum^ k A B A C
16 1 5 mpteq2da φ k B A C = k B A 0
17 16 fveq2d φ sum^ k B A C = sum^ k B A 0
18 1 8 sge0z φ sum^ k B A 0 = 0
19 17 18 eqtrd φ sum^ k B A C = 0
20 19 oveq2d φ sum^ k A C + 𝑒 sum^ k B A C = sum^ k A C + 𝑒 0
21 eqid k A C = k A C
22 1 4 21 fmptdf φ k A C : A 0 +∞
23 7 22 sge0xrcl φ sum^ k A C *
24 xaddid1 sum^ k A C * sum^ k A C + 𝑒 0 = sum^ k A C
25 23 24 syl φ sum^ k A C + 𝑒 0 = sum^ k A C
26 eqidd φ sum^ k A C = sum^ k A C
27 20 25 26 3eqtrrd φ sum^ k A C = sum^ k A C + 𝑒 sum^ k B A C
28 undif A B A B A = B
29 3 28 sylib φ A B A = B
30 29 eqcomd φ B = A B A
31 30 mpteq1d φ k B C = k A B A C
32 31 fveq2d φ sum^ k B C = sum^ k A B A C
33 15 27 32 3eqtr4d φ sum^ k A C = sum^ k B C