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 addid1d
 |-  ( ( 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 addid2d
 |-  ( 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 ) )