# Metamath Proof Explorer

## Theorem fsumsplitsn

Description: Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumsplitsn.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fsumsplitsn.kd ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
fsumsplitsn.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumsplitsn.b ${⊢}{\phi }\to {B}\in {V}$
fsumsplitsn.ba ${⊢}{\phi }\to ¬{B}\in {A}$
fsumsplitsn.c ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
fsumsplitsn.d ${⊢}{k}={B}\to {C}={D}$
fsumsplitsn.dcn ${⊢}{\phi }\to {D}\in ℂ$
Assertion fsumsplitsn ${⊢}{\phi }\to \sum _{{k}\in {A}\cup \left\{{B}\right\}}{C}=\sum _{{k}\in {A}}{C}+{D}$

### Proof

Step Hyp Ref Expression
1 fsumsplitsn.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fsumsplitsn.kd ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
3 fsumsplitsn.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
4 fsumsplitsn.b ${⊢}{\phi }\to {B}\in {V}$
5 fsumsplitsn.ba ${⊢}{\phi }\to ¬{B}\in {A}$
6 fsumsplitsn.c ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
7 fsumsplitsn.d ${⊢}{k}={B}\to {C}={D}$
8 fsumsplitsn.dcn ${⊢}{\phi }\to {D}\in ℂ$
9 disjsn ${⊢}{A}\cap \left\{{B}\right\}=\varnothing ↔¬{B}\in {A}$
10 5 9 sylibr ${⊢}{\phi }\to {A}\cap \left\{{B}\right\}=\varnothing$
11 eqidd ${⊢}{\phi }\to {A}\cup \left\{{B}\right\}={A}\cup \left\{{B}\right\}$
12 snfi ${⊢}\left\{{B}\right\}\in \mathrm{Fin}$
13 unfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \left\{{B}\right\}\in \mathrm{Fin}\right)\to {A}\cup \left\{{B}\right\}\in \mathrm{Fin}$
14 3 12 13 sylancl ${⊢}{\phi }\to {A}\cup \left\{{B}\right\}\in \mathrm{Fin}$
15 6 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({A}\cup \left\{{B}\right\}\right)\right)\wedge {k}\in {A}\right)\to {C}\in ℂ$
16 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({A}\cup \left\{{B}\right\}\right)\right)\wedge ¬{k}\in {A}\right)\to {\phi }$
17 elunnel1 ${⊢}\left({k}\in \left({A}\cup \left\{{B}\right\}\right)\wedge ¬{k}\in {A}\right)\to {k}\in \left\{{B}\right\}$
18 elsni ${⊢}{k}\in \left\{{B}\right\}\to {k}={B}$
19 17 18 syl ${⊢}\left({k}\in \left({A}\cup \left\{{B}\right\}\right)\wedge ¬{k}\in {A}\right)\to {k}={B}$
20 19 adantll ${⊢}\left(\left({\phi }\wedge {k}\in \left({A}\cup \left\{{B}\right\}\right)\right)\wedge ¬{k}\in {A}\right)\to {k}={B}$
21 7 adantl ${⊢}\left({\phi }\wedge {k}={B}\right)\to {C}={D}$
22 8 adantr ${⊢}\left({\phi }\wedge {k}={B}\right)\to {D}\in ℂ$
23 21 22 eqeltrd ${⊢}\left({\phi }\wedge {k}={B}\right)\to {C}\in ℂ$
24 16 20 23 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({A}\cup \left\{{B}\right\}\right)\right)\wedge ¬{k}\in {A}\right)\to {C}\in ℂ$
25 15 24 pm2.61dan ${⊢}\left({\phi }\wedge {k}\in \left({A}\cup \left\{{B}\right\}\right)\right)\to {C}\in ℂ$
26 1 10 11 14 25 fsumsplitf ${⊢}{\phi }\to \sum _{{k}\in {A}\cup \left\{{B}\right\}}{C}=\sum _{{k}\in {A}}{C}+\sum _{{k}\in \left\{{B}\right\}}{C}$
27 2 7 sumsnf ${⊢}\left({B}\in {V}\wedge {D}\in ℂ\right)\to \sum _{{k}\in \left\{{B}\right\}}{C}={D}$
28 4 8 27 syl2anc ${⊢}{\phi }\to \sum _{{k}\in \left\{{B}\right\}}{C}={D}$
29 28 oveq2d ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}+\sum _{{k}\in \left\{{B}\right\}}{C}=\sum _{{k}\in {A}}{C}+{D}$
30 26 29 eqtrd ${⊢}{\phi }\to \sum _{{k}\in {A}\cup \left\{{B}\right\}}{C}=\sum _{{k}\in {A}}{C}+{D}$