This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sumsplit

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

Ref Expression
Hypotheses sumsplit.1 
|- Z = ( ZZ>= ` M )
sumsplit.2 
|- ( ph -> M e. ZZ )
sumsplit.3 
|- ( ph -> ( A i^i B ) = (/) )
sumsplit.4 
|- ( ph -> ( A u. B ) C_ Z )
sumsplit.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , C , 0 ) )
sumsplit.6 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = if ( k e. B , C , 0 ) )
sumsplit.7 
|- ( ( ph /\ k e. ( A u. B ) ) -> C e. CC )
sumsplit.8 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
sumsplit.9 
|- ( ph -> seq M ( + , G ) e. dom ~~> )
Assertion sumsplit 
|- ( ph -> sum_ k e. ( A u. B ) C = ( sum_ k e. A C + sum_ k e. B C ) )

Proof

Step Hyp Ref Expression
1 sumsplit.1 
 |-  Z = ( ZZ>= ` M )
2 sumsplit.2 
 |-  ( ph -> M e. ZZ )
3 sumsplit.3 
 |-  ( ph -> ( A i^i B ) = (/) )
4 sumsplit.4 
 |-  ( ph -> ( A u. B ) C_ Z )
5 sumsplit.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , C , 0 ) )
6 sumsplit.6 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = if ( k e. B , C , 0 ) )
7 sumsplit.7 
 |-  ( ( ph /\ k e. ( A u. B ) ) -> C e. CC )
8 sumsplit.8 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
9 sumsplit.9 
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )
10 7 ralrimiva 
 |-  ( ph -> A. k e. ( A u. B ) C e. CC )
11 1 eqimssi 
 |-  Z C_ ( ZZ>= ` M )
12 11 a1i 
 |-  ( ph -> Z C_ ( ZZ>= ` M ) )
13 12 orcd 
 |-  ( ph -> ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) )
14 sumss2 
 |-  ( ( ( ( A u. B ) C_ Z /\ A. k e. ( A u. B ) C e. CC ) /\ ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) ) -> sum_ k e. ( A u. B ) C = sum_ k e. Z if ( k e. ( A u. B ) , C , 0 ) )
15 4 10 13 14 syl21anc 
 |-  ( ph -> sum_ k e. ( A u. B ) C = sum_ k e. Z if ( k e. ( A u. B ) , C , 0 ) )
16 iftrue 
 |-  ( k e. A -> if ( k e. A , C , 0 ) = C )
17 16 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , C , 0 ) = C )
18 elun1 
 |-  ( k e. A -> k e. ( A u. B ) )
19 18 7 sylan2 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
20 17 19 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , C , 0 ) e. CC )
21 iffalse 
 |-  ( -. k e. A -> if ( k e. A , C , 0 ) = 0 )
22 0cn 
 |-  0 e. CC
23 21 22 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , C , 0 ) e. CC )
24 23 adantl 
 |-  ( ( ph /\ -. k e. A ) -> if ( k e. A , C , 0 ) e. CC )
25 20 24 pm2.61dan 
 |-  ( ph -> if ( k e. A , C , 0 ) e. CC )
26 25 adantr 
 |-  ( ( ph /\ k e. Z ) -> if ( k e. A , C , 0 ) e. CC )
27 iftrue 
 |-  ( k e. B -> if ( k e. B , C , 0 ) = C )
28 27 adantl 
 |-  ( ( ph /\ k e. B ) -> if ( k e. B , C , 0 ) = C )
29 elun2 
 |-  ( k e. B -> k e. ( A u. B ) )
30 29 7 sylan2 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
31 28 30 eqeltrd 
 |-  ( ( ph /\ k e. B ) -> if ( k e. B , C , 0 ) e. CC )
32 iffalse 
 |-  ( -. k e. B -> if ( k e. B , C , 0 ) = 0 )
33 32 22 eqeltrdi 
 |-  ( -. k e. B -> if ( k e. B , C , 0 ) e. CC )
34 33 adantl 
 |-  ( ( ph /\ -. k e. B ) -> if ( k e. B , C , 0 ) e. CC )
35 31 34 pm2.61dan 
 |-  ( ph -> if ( k e. B , C , 0 ) e. CC )
36 35 adantr 
 |-  ( ( ph /\ k e. Z ) -> if ( k e. B , C , 0 ) e. CC )
37 1 2 5 26 6 36 8 9 isumadd 
 |-  ( ph -> sum_ k e. Z ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( sum_ k e. Z if ( k e. A , C , 0 ) + sum_ k e. Z if ( k e. B , C , 0 ) ) )
38 19 addridd 
 |-  ( ( ph /\ k e. A ) -> ( C + 0 ) = C )
39 noel 
 |-  -. k e. (/)
40 3 eleq2d 
 |-  ( ph -> ( k e. ( A i^i B ) <-> k e. (/) ) )
41 elin 
 |-  ( k e. ( A i^i B ) <-> ( k e. A /\ k e. B ) )
42 40 41 bitr3di 
 |-  ( ph -> ( k e. (/) <-> ( k e. A /\ k e. B ) ) )
43 39 42 mtbii 
 |-  ( ph -> -. ( k e. A /\ k e. B ) )
44 imnan 
 |-  ( ( k e. A -> -. k e. B ) <-> -. ( k e. A /\ k e. B ) )
45 43 44 sylibr 
 |-  ( ph -> ( k e. A -> -. k e. B ) )
46 45 imp 
 |-  ( ( ph /\ k e. A ) -> -. k e. B )
47 46 32 syl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. B , C , 0 ) = 0 )
48 17 47 oveq12d 
 |-  ( ( ph /\ k e. A ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( C + 0 ) )
49 iftrue 
 |-  ( k e. ( A u. B ) -> if ( k e. ( A u. B ) , C , 0 ) = C )
50 18 49 syl 
 |-  ( k e. A -> if ( k e. ( A u. B ) , C , 0 ) = C )
51 50 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. ( A u. B ) , C , 0 ) = C )
52 38 48 51 3eqtr4rd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. ( A u. B ) , C , 0 ) = ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) )
53 35 addlidd 
 |-  ( ph -> ( 0 + if ( k e. B , C , 0 ) ) = if ( k e. B , C , 0 ) )
54 53 adantr 
 |-  ( ( ph /\ -. k e. A ) -> ( 0 + if ( k e. B , C , 0 ) ) = if ( k e. B , C , 0 ) )
55 21 adantl 
 |-  ( ( ph /\ -. k e. A ) -> if ( k e. A , C , 0 ) = 0 )
56 55 oveq1d 
 |-  ( ( ph /\ -. k e. A ) -> ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) = ( 0 + if ( k e. B , C , 0 ) ) )
57 elun 
 |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )
58 biorf 
 |-  ( -. k e. A -> ( k e. B <-> ( k e. A \/ k e. B ) ) )
59 57 58 bitr4id 
 |-  ( -. k e. A -> ( k e. ( A u. B ) <-> k e. B ) )
60 59 adantl 
 |-  ( ( ph /\ -. k e. A ) -> ( k e. ( A u. B ) <-> k e. B ) )
61 60 ifbid 
 |-  ( ( ph /\ -. k e. A ) -> if ( k e. ( A u. B ) , C , 0 ) = if ( k e. B , C , 0 ) )
62 54 56 61 3eqtr4rd 
 |-  ( ( ph /\ -. k e. A ) -> if ( k e. ( A u. B ) , C , 0 ) = ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) )
63 52 62 pm2.61dan 
 |-  ( ph -> if ( k e. ( A u. B ) , C , 0 ) = ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) )
64 63 sumeq2sdv 
 |-  ( ph -> sum_ k e. Z if ( k e. ( A u. B ) , C , 0 ) = sum_ k e. Z ( if ( k e. A , C , 0 ) + if ( k e. B , C , 0 ) ) )
65 4 unssad 
 |-  ( ph -> A C_ Z )
66 19 ralrimiva 
 |-  ( ph -> A. k e. A C e. CC )
67 sumss2 
 |-  ( ( ( A C_ Z /\ A. k e. A C e. CC ) /\ ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) ) -> sum_ k e. A C = sum_ k e. Z if ( k e. A , C , 0 ) )
68 65 66 13 67 syl21anc 
 |-  ( ph -> sum_ k e. A C = sum_ k e. Z if ( k e. A , C , 0 ) )
69 4 unssbd 
 |-  ( ph -> B C_ Z )
70 30 ralrimiva 
 |-  ( ph -> A. k e. B C e. CC )
71 sumss2 
 |-  ( ( ( B C_ Z /\ A. k e. B C e. CC ) /\ ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) ) -> sum_ k e. B C = sum_ k e. Z if ( k e. B , C , 0 ) )
72 69 70 13 71 syl21anc 
 |-  ( ph -> sum_ k e. B C = sum_ k e. Z if ( k e. B , C , 0 ) )
73 68 72 oveq12d 
 |-  ( ph -> ( sum_ k e. A C + sum_ k e. B C ) = ( sum_ k e. Z if ( k e. A , C , 0 ) + sum_ k e. Z if ( k e. B , C , 0 ) ) )
74 37 64 73 3eqtr4rd 
 |-  ( ph -> ( sum_ k e. A C + sum_ k e. B C ) = sum_ k e. Z if ( k e. ( A u. B ) , C , 0 ) )
75 15 74 eqtr4d 
 |-  ( ph -> sum_ k e. ( A u. B ) C = ( sum_ k e. A C + sum_ k e. B C ) )