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 xaddrid ⊢ 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