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 eqtrdi
 |-  ( 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 ) )