Metamath Proof Explorer

Theorem sge0splitmpt

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0splitmpt.xph ⊢ Ⅎ x φ
sge0splitmpt.a ⊢ φ → A ∈ V
sge0splitmpt.b ⊢ φ → B ∈ W
sge0splitmpt.in ⊢ φ → A ∩ B = ∅
sge0splitmpt.ac ⊢ φ ∧ x ∈ A → C ∈ 0 +∞
sge0splitmpt.bc ⊢ φ ∧ x ∈ B → C ∈ 0 +∞
Assertion sge0splitmpt ⊢ φ → sum^ ⁡ x ∈ A ∪ B ⟼ C = sum^ ⁡ x ∈ A ⟼ C + 𝑒 sum^ ⁡ x ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 sge0splitmpt.xph ⊢ Ⅎ x φ
2 sge0splitmpt.a ⊢ φ → A ∈ V
3 sge0splitmpt.b ⊢ φ → B ∈ W
4 sge0splitmpt.in ⊢ φ → A ∩ B = ∅
5 sge0splitmpt.ac ⊢ φ ∧ x ∈ A → C ∈ 0 +∞
6 sge0splitmpt.bc ⊢ φ ∧ x ∈ B → C ∈ 0 +∞
7 eqid ⊢ A ∪ B = A ∪ B
8 5 adantlr ⊢ φ ∧ x ∈ A ∪ B ∧ x ∈ A → C ∈ 0 +∞
9 simpll ⊢ φ ∧ x ∈ A ∪ B ∧ ¬ x ∈ A → φ
10 elunnel1 ⊢ x ∈ A ∪ B ∧ ¬ x ∈ A → x ∈ B
11 10 adantll ⊢ φ ∧ x ∈ A ∪ B ∧ ¬ x ∈ A → x ∈ B
12 9 11 6 syl2anc ⊢ φ ∧ x ∈ A ∪ B ∧ ¬ x ∈ A → C ∈ 0 +∞
13 8 12 pm2.61dan ⊢ φ ∧ x ∈ A ∪ B → C ∈ 0 +∞
14 eqid ⊢ x ∈ A ∪ B ⟼ C = x ∈ A ∪ B ⟼ C
15 1 13 14 fmptdf ⊢ φ → x ∈ A ∪ B ⟼ C : A ∪ B ⟶ 0 +∞
16 2 3 7 4 15 sge0split ⊢ φ → sum^ ⁡ x ∈ A ∪ B ⟼ C = sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ A + 𝑒 sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ B
17 ssun1 ⊢ A ⊆ A ∪ B
18 17 resmpti ⊢ x ∈ A ∪ B ⟼ C ↾ A = x ∈ A ⟼ C
19 18 fveq2i ⊢ sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ A = sum^ ⁡ x ∈ A ⟼ C
20 ssun2 ⊢ B ⊆ A ∪ B
21 20 resmpti ⊢ x ∈ A ∪ B ⟼ C ↾ B = x ∈ B ⟼ C
22 21 fveq2i ⊢ sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ B = sum^ ⁡ x ∈ B ⟼ C
23 19 22 oveq12i ⊢ sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ A + 𝑒 sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ B = sum^ ⁡ x ∈ A ⟼ C + 𝑒 sum^ ⁡ x ∈ B ⟼ C
24 23 a1i ⊢ φ → sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ A + 𝑒 sum^ ⁡ x ∈ A ∪ B ⟼ C ↾ B = sum^ ⁡ x ∈ A ⟼ C + 𝑒 sum^ ⁡ x ∈ B ⟼ C
25 16 24 eqtrd ⊢ φ → sum^ ⁡ x ∈ A ∪ B ⟼ C = sum^ ⁡ x ∈ A ⟼ C + 𝑒 sum^ ⁡ x ∈ B ⟼ C