# Metamath Proof Explorer

## Theorem fsumsplit

Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumsplit.1 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
fsumsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
fsumsplit.3 ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
fsumsplit.4 ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
Assertion fsumsplit ${⊢}{\phi }\to \sum _{{k}\in {U}}{C}=\sum _{{k}\in {A}}{C}+\sum _{{k}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 fsumsplit.1 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
2 fsumsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
3 fsumsplit.3 ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
4 fsumsplit.4 ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
5 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
6 5 2 sseqtrrid ${⊢}{\phi }\to {A}\subseteq {U}$
7 6 sselda ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {U}$
8 7 4 syldan ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
9 8 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in ℂ$
10 3 olcd ${⊢}{\phi }\to \left({U}\subseteq {ℤ}_{\ge 0}\vee {U}\in \mathrm{Fin}\right)$
11 sumss2 ${⊢}\left(\left({A}\subseteq {U}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in ℂ\right)\wedge \left({U}\subseteq {ℤ}_{\ge 0}\vee {U}\in \mathrm{Fin}\right)\right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {U}}if\left({k}\in {A},{C},0\right)$
12 6 9 10 11 syl21anc ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {U}}if\left({k}\in {A},{C},0\right)$
13 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
14 13 2 sseqtrrid ${⊢}{\phi }\to {B}\subseteq {U}$
15 14 sselda ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {k}\in {U}$
16 15 4 syldan ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {C}\in ℂ$
17 16 ralrimiva ${⊢}{\phi }\to \forall {k}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in ℂ$
18 sumss2 ${⊢}\left(\left({B}\subseteq {U}\wedge \forall {k}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in ℂ\right)\wedge \left({U}\subseteq {ℤ}_{\ge 0}\vee {U}\in \mathrm{Fin}\right)\right)\to \sum _{{k}\in {B}}{C}=\sum _{{k}\in {U}}if\left({k}\in {B},{C},0\right)$
19 14 17 10 18 syl21anc ${⊢}{\phi }\to \sum _{{k}\in {B}}{C}=\sum _{{k}\in {U}}if\left({k}\in {B},{C},0\right)$
20 12 19 oveq12d ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}+\sum _{{k}\in {B}}{C}=\sum _{{k}\in {U}}if\left({k}\in {A},{C},0\right)+\sum _{{k}\in {U}}if\left({k}\in {B},{C},0\right)$
21 0cn ${⊢}0\in ℂ$
22 ifcl ${⊢}\left({C}\in ℂ\wedge 0\in ℂ\right)\to if\left({k}\in {A},{C},0\right)\in ℂ$
23 4 21 22 sylancl ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {A},{C},0\right)\in ℂ$
24 ifcl ${⊢}\left({C}\in ℂ\wedge 0\in ℂ\right)\to if\left({k}\in {B},{C},0\right)\in ℂ$
25 4 21 24 sylancl ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {B},{C},0\right)\in ℂ$
26 3 23 25 fsumadd ${⊢}{\phi }\to \sum _{{k}\in {U}}\left(if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)\right)=\sum _{{k}\in {U}}if\left({k}\in {A},{C},0\right)+\sum _{{k}\in {U}}if\left({k}\in {B},{C},0\right)$
27 2 eleq2d ${⊢}{\phi }\to \left({k}\in {U}↔{k}\in \left({A}\cup {B}\right)\right)$
28 elun ${⊢}{k}\in \left({A}\cup {B}\right)↔\left({k}\in {A}\vee {k}\in {B}\right)$
29 27 28 syl6bb ${⊢}{\phi }\to \left({k}\in {U}↔\left({k}\in {A}\vee {k}\in {B}\right)\right)$
30 29 biimpa ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to \left({k}\in {A}\vee {k}\in {B}\right)$
31 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{C},0\right)={C}$
32 31 adantl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},0\right)={C}$
33 noel ${⊢}¬{k}\in \varnothing$
34 elin ${⊢}{k}\in \left({A}\cap {B}\right)↔\left({k}\in {A}\wedge {k}\in {B}\right)$
35 1 eleq2d ${⊢}{\phi }\to \left({k}\in \left({A}\cap {B}\right)↔{k}\in \varnothing \right)$
36 34 35 syl5rbbr ${⊢}{\phi }\to \left({k}\in \varnothing ↔\left({k}\in {A}\wedge {k}\in {B}\right)\right)$
37 33 36 mtbii ${⊢}{\phi }\to ¬\left({k}\in {A}\wedge {k}\in {B}\right)$
38 imnan ${⊢}\left({k}\in {A}\to ¬{k}\in {B}\right)↔¬\left({k}\in {A}\wedge {k}\in {B}\right)$
39 37 38 sylibr ${⊢}{\phi }\to \left({k}\in {A}\to ¬{k}\in {B}\right)$
40 39 imp ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬{k}\in {B}$
41 40 iffalsed ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {B},{C},0\right)=0$
42 32 41 oveq12d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)={C}+0$
43 8 addid1d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}+0={C}$
44 42 43 eqtrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)={C}$
45 39 con2d ${⊢}{\phi }\to \left({k}\in {B}\to ¬{k}\in {A}\right)$
46 45 imp ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to ¬{k}\in {A}$
47 46 iffalsed ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},0\right)=0$
48 iftrue ${⊢}{k}\in {B}\to if\left({k}\in {B},{C},0\right)={C}$
49 48 adantl ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {B},{C},0\right)={C}$
50 47 49 oveq12d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)=0+{C}$
51 16 addid2d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to 0+{C}={C}$
52 50 51 eqtrd ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)={C}$
53 44 52 jaodan ${⊢}\left({\phi }\wedge \left({k}\in {A}\vee {k}\in {B}\right)\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)={C}$
54 30 53 syldan ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)={C}$
55 54 sumeq2dv ${⊢}{\phi }\to \sum _{{k}\in {U}}\left(if\left({k}\in {A},{C},0\right)+if\left({k}\in {B},{C},0\right)\right)=\sum _{{k}\in {U}}{C}$
56 20 26 55 3eqtr2rd ${⊢}{\phi }\to \sum _{{k}\in {U}}{C}=\sum _{{k}\in {A}}{C}+\sum _{{k}\in {B}}{C}$