# Metamath Proof Explorer

## Theorem fsumsplit1

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

Ref Expression
Hypotheses fsumsplit1.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fsumsplit1.kd ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
fsumsplit1.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumsplit1.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fsumsplit1.c ${⊢}{\phi }\to {C}\in {A}$
fsumsplit1.bd ${⊢}{k}={C}\to {B}={D}$
Assertion fsumsplit1 ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}={D}+\sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}$

### Proof

Step Hyp Ref Expression
1 fsumsplit1.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fsumsplit1.kd ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
3 fsumsplit1.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
4 fsumsplit1.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
5 fsumsplit1.c ${⊢}{\phi }\to {C}\in {A}$
6 fsumsplit1.bd ${⊢}{k}={C}\to {B}={D}$
7 uncom ${⊢}\left({A}\setminus \left\{{C}\right\}\right)\cup \left\{{C}\right\}=\left\{{C}\right\}\cup \left({A}\setminus \left\{{C}\right\}\right)$
8 7 a1i ${⊢}{\phi }\to \left({A}\setminus \left\{{C}\right\}\right)\cup \left\{{C}\right\}=\left\{{C}\right\}\cup \left({A}\setminus \left\{{C}\right\}\right)$
9 5 snssd ${⊢}{\phi }\to \left\{{C}\right\}\subseteq {A}$
10 undif ${⊢}\left\{{C}\right\}\subseteq {A}↔\left\{{C}\right\}\cup \left({A}\setminus \left\{{C}\right\}\right)={A}$
11 9 10 sylib ${⊢}{\phi }\to \left\{{C}\right\}\cup \left({A}\setminus \left\{{C}\right\}\right)={A}$
12 eqidd ${⊢}{\phi }\to {A}={A}$
13 8 11 12 3eqtrrd ${⊢}{\phi }\to {A}=\left({A}\setminus \left\{{C}\right\}\right)\cup \left\{{C}\right\}$
14 13 sumeq1d ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{k}\in \left({A}\setminus \left\{{C}\right\}\right)\cup \left\{{C}\right\}}{B}$
15 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{C}\right\}\in \mathrm{Fin}$
16 3 15 syl ${⊢}{\phi }\to {A}\setminus \left\{{C}\right\}\in \mathrm{Fin}$
17 neldifsnd ${⊢}{\phi }\to ¬{C}\in \left({A}\setminus \left\{{C}\right\}\right)$
18 simpl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{C}\right\}\right)\right)\to {\phi }$
19 eldifi ${⊢}{k}\in \left({A}\setminus \left\{{C}\right\}\right)\to {k}\in {A}$
20 19 adantl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{C}\right\}\right)\right)\to {k}\in {A}$
21 18 20 4 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{C}\right\}\right)\right)\to {B}\in ℂ$
22 2 a1i ${⊢}{\phi }\to \underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
23 simpr ${⊢}\left({\phi }\wedge {k}={C}\right)\to {k}={C}$
24 23 6 syl ${⊢}\left({\phi }\wedge {k}={C}\right)\to {B}={D}$
25 1 22 5 24 csbiedf
26 25 eqcomd
27 5 ancli ${⊢}{\phi }\to \left({\phi }\wedge {C}\in {A}\right)$
28 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{C}$
29 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{C}\in {A}$
30 1 29 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {C}\in {A}\right)$
31 28 nfcsb1
32 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℂ$
33 31 32 nfel
34 30 33 nfim
35 eleq1 ${⊢}{k}={C}\to \left({k}\in {A}↔{C}\in {A}\right)$
36 35 anbi2d ${⊢}{k}={C}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {C}\in {A}\right)\right)$
37 csbeq1a
38 37 eleq1d
39 36 38 imbi12d
40 28 34 39 4 vtoclgf
41 5 27 40 sylc
42 26 41 eqeltrd ${⊢}{\phi }\to {D}\in ℂ$
43 1 2 16 5 17 21 6 42 fsumsplitsn ${⊢}{\phi }\to \sum _{{k}\in \left({A}\setminus \left\{{C}\right\}\right)\cup \left\{{C}\right\}}{B}=\sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}+{D}$
44 1 16 21 fsumclf ${⊢}{\phi }\to \sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}\in ℂ$
45 44 42 addcomd ${⊢}{\phi }\to \sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}+{D}={D}+\sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}$
46 14 43 45 3eqtrd ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}={D}+\sum _{{k}\in {A}\setminus \left\{{C}\right\}}{B}$