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