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