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 
|- F/ k ph
fsumsplitf.ab 
|- ( ph -> ( A i^i B ) = (/) )
fsumsplitf.u 
|- ( ph -> U = ( A u. B ) )
fsumsplitf.fi 
|- ( ph -> U e. Fin )
fsumsplitf.c 
|- ( ( ph /\ k e. U ) -> C e. CC )
Assertion fsumsplitf 
|- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )

Proof

Step Hyp Ref Expression
1 fsumsplitf.ph 
 |-  F/ k ph
2 fsumsplitf.ab 
 |-  ( ph -> ( A i^i B ) = (/) )
3 fsumsplitf.u 
 |-  ( ph -> U = ( A u. B ) )
4 fsumsplitf.fi 
 |-  ( ph -> U e. Fin )
5 fsumsplitf.c 
 |-  ( ( ph /\ k e. U ) -> C e. CC )
6 nfcv 
 |-  F/_ j C
7 nfcsb1v 
 |-  F/_ k [_ j / k ]_ C
8 csbeq1a 
 |-  ( k = j -> C = [_ j / k ]_ C )
9 6 7 8 cbvsumi 
 |-  sum_ k e. U C = sum_ j e. U [_ j / k ]_ C
10 9 a1i 
 |-  ( ph -> sum_ k e. U C = sum_ j e. U [_ j / k ]_ C )
11 nfv 
 |-  F/ k j e. U
12 1 11 nfan 
 |-  F/ k ( ph /\ j e. U )
13 7 nfel1 
 |-  F/ k [_ j / k ]_ C e. CC
14 12 13 nfim 
 |-  F/ k ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC )
15 eleq1w 
 |-  ( k = j -> ( k e. U <-> j e. U ) )
16 15 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. U ) <-> ( ph /\ j e. U ) ) )
17 8 eleq1d 
 |-  ( k = j -> ( C e. CC <-> [_ j / k ]_ C e. CC ) )
18 16 17 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. U ) -> C e. CC ) <-> ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC ) ) )
19 14 18 5 chvarfv 
 |-  ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC )
20 2 3 4 19 fsumsplit 
 |-  ( ph -> sum_ j e. U [_ j / k ]_ C = ( sum_ j e. A [_ j / k ]_ C + sum_ j e. B [_ j / k ]_ C ) )
21 csbeq1a 
 |-  ( j = k -> [_ j / k ]_ C = [_ k / j ]_ [_ j / k ]_ C )
22 csbcow 
 |-  [_ k / j ]_ [_ j / k ]_ C = [_ k / k ]_ C
23 csbid 
 |-  [_ k / k ]_ C = C
24 22 23 eqtri 
 |-  [_ k / j ]_ [_ j / k ]_ C = C
25 21 24 syl6eq 
 |-  ( j = k -> [_ j / k ]_ C = C )
26 7 6 25 cbvsumi 
 |-  sum_ j e. A [_ j / k ]_ C = sum_ k e. A C
27 7 6 25 cbvsumi 
 |-  sum_ j e. B [_ j / k ]_ C = sum_ k e. B C
28 26 27 oveq12i 
 |-  ( sum_ j e. A [_ j / k ]_ C + sum_ j e. B [_ j / k ]_ C ) = ( sum_ k e. A C + sum_ k e. B C )
29 28 a1i 
 |-  ( ph -> ( sum_ j e. A [_ j / k ]_ C + sum_ j e. B [_ j / k ]_ C ) = ( sum_ k e. A C + sum_ k e. B C ) )
30 10 20 29 3eqtrd 
 |-  ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )