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 difexg ⊢ B ∈ V → B ∖ A ∈ V
9 2 8 syl ⊢ φ → B ∖ A ∈ V
10 disjdif ⊢ A ∩ B ∖ A = ∅
11 10 a1i ⊢ φ → A ∩ B ∖ A = ∅
12 0e0iccpnf ⊢ 0 ∈ 0 +∞
13 12 a1i ⊢ φ ∧ k ∈ B ∖ A → 0 ∈ 0 +∞
14 5 13 eqeltrd ⊢ φ ∧ k ∈ B ∖ A → C ∈ 0 +∞
15 1 7 9 11 4 14 sge0splitmpt ⊢ φ → sum^ ⁡ k ∈ A ∪ B ∖ A ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ∖ A ⟼ C
16 15 eqcomd ⊢ φ → sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ∖ A ⟼ C = sum^ ⁡ k ∈ A ∪ B ∖ A ⟼ C
17 1 5 mpteq2da ⊢ φ → k ∈ B ∖ A ⟼ C = k ∈ B ∖ A ⟼ 0
18 17 fveq2d ⊢ φ → sum^ ⁡ k ∈ B ∖ A ⟼ C = sum^ ⁡ k ∈ B ∖ A ⟼ 0
19 1 9 sge0z ⊢ φ → sum^ ⁡ k ∈ B ∖ A ⟼ 0 = 0
20 18 19 eqtrd ⊢ φ → sum^ ⁡ k ∈ B ∖ A ⟼ C = 0
21 20 oveq2d ⊢ φ → sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ∖ A ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 0
22 eqid ⊢ k ∈ A ⟼ C = k ∈ A ⟼ C
23 1 4 22 fmptdf ⊢ φ → k ∈ A ⟼ C : A ⟶ 0 +∞
24 7 23 sge0xrcl ⊢ φ → sum^ ⁡ k ∈ A ⟼ C ∈ ℝ *
25 xaddid1 ⊢ sum^ ⁡ k ∈ A ⟼ C ∈ ℝ * → sum^ ⁡ k ∈ A ⟼ C + 𝑒 0 = sum^ ⁡ k ∈ A ⟼ C
26 24 25 syl ⊢ φ → sum^ ⁡ k ∈ A ⟼ C + 𝑒 0 = sum^ ⁡ k ∈ A ⟼ C
27 eqidd ⊢ φ → sum^ ⁡ k ∈ A ⟼ C = sum^ ⁡ k ∈ A ⟼ C
28 21 26 27 3eqtrrd ⊢ φ → sum^ ⁡ k ∈ A ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ∖ A ⟼ C
29 undif ⊢ A ⊆ B ↔ A ∪ B ∖ A = B
30 3 29 sylib ⊢ φ → A ∪ B ∖ A = B
31 30 eqcomd ⊢ φ → B = A ∪ B ∖ A
32 31 mpteq1d ⊢ φ → k ∈ B ⟼ C = k ∈ A ∪ B ∖ A ⟼ C
33 32 fveq2d ⊢ φ → sum^ ⁡ k ∈ B ⟼ C = sum^ ⁡ k ∈ A ∪ B ∖ A ⟼ C
34 16 28 33 3eqtr4d ⊢ φ → sum^ ⁡ k ∈ A ⟼ C = sum^ ⁡ k ∈ B ⟼ C