Metamath Proof Explorer

Theorem sge0splitsn

Description: Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0splitsn.ph ⊢ Ⅎ k φ
sge0splitsn.a ⊢ φ → A ∈ V
sge0splitsn.b ⊢ φ → B ∈ W
sge0splitsn.n ⊢ φ → ¬ B ∈ A
sge0splitsn.c ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
sge0splitsn.d ⊢ k = B → C = D
sge0splitsn.e ⊢ φ → D ∈ 0 +∞
Assertion sge0splitsn ⊢ φ → sum^ ⁡ k ∈ A ∪ B ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 D

Proof

Step Hyp Ref Expression
1 sge0splitsn.ph ⊢ Ⅎ k φ
2 sge0splitsn.a ⊢ φ → A ∈ V
3 sge0splitsn.b ⊢ φ → B ∈ W
4 sge0splitsn.n ⊢ φ → ¬ B ∈ A
5 sge0splitsn.c ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
6 sge0splitsn.d ⊢ k = B → C = D
7 sge0splitsn.e ⊢ φ → D ∈ 0 +∞
8 snfi ⊢ B ∈ Fin
9 8 a1i ⊢ φ → B ∈ Fin
10 9 elexd ⊢ φ → B ∈ V
11 disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A
12 4 11 sylibr ⊢ φ → A ∩ B = ∅
13 elsni ⊢ k ∈ B → k = B
14 6 adantl ⊢ φ ∧ k = B → C = D
15 13 14 sylan2 ⊢ φ ∧ k ∈ B → C = D
16 7 adantr ⊢ φ ∧ k ∈ B → D ∈ 0 +∞
17 15 16 eqeltrd ⊢ φ ∧ k ∈ B → C ∈ 0 +∞
18 1 2 10 12 5 17 sge0splitmpt ⊢ φ → sum^ ⁡ k ∈ A ∪ B ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ⟼ C
19 1 3 7 6 sge0snmptf ⊢ φ → sum^ ⁡ k ∈ B ⟼ C = D
20 19 oveq2d ⊢ φ → sum^ ⁡ k ∈ A ⟼ C + 𝑒 sum^ ⁡ k ∈ B ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 D
21 18 20 eqtrd ⊢ φ → sum^ ⁡ k ∈ A ∪ B ⟼ C = sum^ ⁡ k ∈ A ⟼ C + 𝑒 D