Metamath Proof Explorer


Theorem fsumsplit

Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumsplit.1
|- ( ph -> ( A i^i B ) = (/) )
fsumsplit.2
|- ( ph -> U = ( A u. B ) )
fsumsplit.3
|- ( ph -> U e. Fin )
fsumsplit.4
|- ( ( ph /\ k e. U ) -> C e. CC )
Assertion fsumsplit
|- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )

Proof

Step Hyp Ref Expression
1 fsumsplit.1
 |-  ( ph -> ( A i^i B ) = (/) )
2 fsumsplit.2
 |-  ( ph -> U = ( A u. B ) )
3 fsumsplit.3
 |-  ( ph -> U e. Fin )
4 fsumsplit.4
 |-  ( ( ph /\ k e. U ) -> C e. CC )
5 ssun1
 |-  A C_ ( A u. B )
6 5 2 sseqtrrid
 |-  ( ph -> A C_ U )
7 6 sselda
 |-  ( ( ph /\ k e. A ) -> k e. U )
8 7 4 syldan
 |-  ( ( ph /\ k e. A ) -> C e. CC )
9 8 ralrimiva
 |-  ( ph -> A. k e. A C e. CC )
10 3 olcd
 |-  ( ph -> ( U C_ ( ZZ>= ` 0 ) \/ U e. Fin ) )
11 sumss2
 |-  ( ( ( A C_ U /\ A. k e. A C e. CC ) /\ ( U C_ ( ZZ>= ` 0 ) \/ U e. Fin ) ) -> sum_ k e. A C = sum_ k e. U if ( k e. A , C , 0 ) )
12 6 9 10 11 syl21anc
 |-  ( ph -> sum_ k e. A C = sum_ k e. U if ( k e. A , C , 0 ) )
13 ssun2
 |-  B C_ ( A u. B )
14 13 2 sseqtrrid
 |-  ( ph -> B C_ U )
15 14 sselda
 |-  ( ( ph /\ k e. B ) -> k e. U )
16 15 4 syldan
 |-  ( ( ph /\ k e. B ) -> C e. CC )
17 16 ralrimiva
 |-  ( ph -> A. k e. B C e. CC )
18 sumss2
 |-  ( ( ( B C_ U /\ A. k e. B C e. CC ) /\ ( U C_ ( ZZ>= ` 0 ) \/ U e. Fin ) ) -> sum_ k e. B C = sum_ k e. U if ( k e. B , C , 0 ) )
19 14 17 10 18 syl21anc
 |-  ( ph -> sum_ k e. B C = sum_ k e. U if ( k e. B , C , 0 ) )
20 12 19 oveq12d
 |-  ( ph -> ( sum_ k e. A C + sum_ k e. B C ) = ( sum_ k e. U if ( k e. A , C , 0 ) + sum_ k e. U if ( k e. B , C , 0 ) ) )
21 0cn
 |-  0 e. CC
22 ifcl
 |-  ( ( C e. CC /\ 0 e. CC ) -> if ( k e. A , C , 0 ) e. CC )
23 4 21 22 sylancl
 |-  ( ( ph /\ k e. U ) -> if ( k e. A , C , 0 ) e. CC )
24 ifcl
 |-  ( ( C e. CC /\ 0 e. CC ) -> if ( k e. B , C , 0 ) e. CC )
25 4 21 24 sylancl
 |-  ( ( ph /\ k e. U ) -> if ( k e. B , C , 0 ) e. CC )
26 3 23 25 fsumadd
 |-  ( ph -> sum_ k e. U ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( sum_ k e. U if ( k e. A , C , 0 ) + sum_ k e. U if ( k e. B , C , 0 ) ) )
27 2 eleq2d
 |-  ( ph -> ( k e. U <-> k e. ( A u. B ) ) )
28 elun
 |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )
29 27 28 bitrdi
 |-  ( ph -> ( k e. U <-> ( k e. A \/ k e. B ) ) )
30 29 biimpa
 |-  ( ( ph /\ k e. U ) -> ( k e. A \/ k e. B ) )
31 iftrue
 |-  ( k e. A -> if ( k e. A , C , 0 ) = C )
32 31 adantl
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , C , 0 ) = C )
33 noel
 |-  -. k e. (/)
34 1 eleq2d
 |-  ( ph -> ( k e. ( A i^i B ) <-> k e. (/) ) )
35 elin
 |-  ( k e. ( A i^i B ) <-> ( k e. A /\ k e. B ) )
36 34 35 bitr3di
 |-  ( ph -> ( k e. (/) <-> ( k e. A /\ k e. B ) ) )
37 33 36 mtbii
 |-  ( ph -> -. ( k e. A /\ k e. B ) )
38 imnan
 |-  ( ( k e. A -> -. k e. B ) <-> -. ( k e. A /\ k e. B ) )
39 37 38 sylibr
 |-  ( ph -> ( k e. A -> -. k e. B ) )
40 39 imp
 |-  ( ( ph /\ k e. A ) -> -. k e. B )
41 40 iffalsed
 |-  ( ( ph /\ k e. A ) -> if ( k e. B , C , 0 ) = 0 )
42 32 41 oveq12d
 |-  ( ( ph /\ k e. A ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( C + 0 ) )
43 8 addid1d
 |-  ( ( ph /\ k e. A ) -> ( C + 0 ) = C )
44 42 43 eqtrd
 |-  ( ( ph /\ k e. A ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = C )
45 39 con2d
 |-  ( ph -> ( k e. B -> -. k e. A ) )
46 45 imp
 |-  ( ( ph /\ k e. B ) -> -. k e. A )
47 46 iffalsed
 |-  ( ( ph /\ k e. B ) -> if ( k e. A , C , 0 ) = 0 )
48 iftrue
 |-  ( k e. B -> if ( k e. B , C , 0 ) = C )
49 48 adantl
 |-  ( ( ph /\ k e. B ) -> if ( k e. B , C , 0 ) = C )
50 47 49 oveq12d
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( 0 + C ) )
51 16 addid2d
 |-  ( ( ph /\ k e. B ) -> ( 0 + C ) = C )
52 50 51 eqtrd
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = C )
53 44 52 jaodan
 |-  ( ( ph /\ ( k e. A \/ k e. B ) ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = C )
54 30 53 syldan
 |-  ( ( ph /\ k e. U ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = C )
55 54 sumeq2dv
 |-  ( ph -> sum_ k e. U ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = sum_ k e. U C )
56 20 26 55 3eqtr2rd
 |-  ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )