# Metamath Proof Explorer

## Theorem fsumsplitf

Description: Split a sum into two parts. A version of fsumsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumsplitf.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fsumsplitf.ab ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
fsumsplitf.u ${⊢}{\phi }\to {U}={A}\cup {B}$
fsumsplitf.fi ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
fsumsplitf.c ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
Assertion fsumsplitf ${⊢}{\phi }\to \sum _{{k}\in {U}}{C}=\sum _{{k}\in {A}}{C}+\sum _{{k}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 fsumsplitf.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fsumsplitf.ab ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
3 fsumsplitf.u ${⊢}{\phi }\to {U}={A}\cup {B}$
4 fsumsplitf.fi ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
5 fsumsplitf.c ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
6 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
7 nfcsb1v
8 csbeq1a
9 6 7 8 cbvsumi
10 9 a1i
11 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{j}\in {U}$
12 1 11 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {U}\right)$
13 7 nfel1
14 12 13 nfim
15 eleq1w ${⊢}{k}={j}\to \left({k}\in {U}↔{j}\in {U}\right)$
16 15 anbi2d ${⊢}{k}={j}\to \left(\left({\phi }\wedge {k}\in {U}\right)↔\left({\phi }\wedge {j}\in {U}\right)\right)$
17 8 eleq1d
18 16 17 imbi12d
19 14 18 5 chvarfv
20 2 3 4 19 fsumsplit
21 csbeq1a
22 csbcow
23 csbid
24 22 23 eqtri
25 21 24 eqtrdi
26 7 6 25 cbvsumi
27 7 6 25 cbvsumi
28 26 27 oveq12i
29 28 a1i
30 10 20 29 3eqtrd ${⊢}{\phi }\to \sum _{{k}\in {U}}{C}=\sum _{{k}\in {A}}{C}+\sum _{{k}\in {B}}{C}$