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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
sumsplit.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sumsplit.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
sumsplit.4 ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑍 )
sumsplit.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
sumsplit.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
sumsplit.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ℂ )
sumsplit.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
sumsplit.9 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
Assertion sumsplit ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step Hyp Ref Expression
1 sumsplit.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 sumsplit.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 sumsplit.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
4 sumsplit.4 ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑍 )
5 sumsplit.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
6 sumsplit.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
7 sumsplit.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ℂ )
8 sumsplit.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
9 sumsplit.9 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
10 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 ∈ ℂ )
11 1 eqimssi ⊢ 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 )
12 11 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) )
13 12 orcd ⊢ ( 𝜑 → ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) )
14 sumss2 ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑍 ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 ∈ ℂ ) ∧ ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) )
15 4 10 13 14 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) )
16 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
18 elun1 ⊢ ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) )
19 18 7 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
20 17 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
21 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
22 0cn ⊢ 0 ∈ ℂ
23 21 22 eqeltrdi ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
24 23 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
25 20 24 pm2.61dan ⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
27 iftrue ⊢ ( 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 𝐶 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 𝐶 )
29 elun2 ⊢ ( 𝑘 ∈ 𝐵 → 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) )
30 29 7 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
31 28 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
32 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 0 )
33 32 22 eqeltrdi ⊢ ( ¬ 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
34 33 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
35 31 34 pm2.61dan ⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
37 1 2 5 26 6 36 8 9 isumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
38 19 addid1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 + 0 ) = 𝐶 )
39 noel ⊢ ¬ 𝑘 ∈ ∅
40 3 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ↔ 𝑘 ∈ ∅ ) )
41 elin ⊢ ( 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
42 40 41 bitr3di ⊢ ( 𝜑 → ( 𝑘 ∈ ∅ ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
43 39 42 mtbii ⊢ ( 𝜑 → ¬ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
44 imnan ⊢ ( ( 𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵 ) ↔ ¬ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
45 43 44 sylibr ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵 ) )
46 45 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 ∈ 𝐵 )
47 46 32 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 0 )
48 17 47 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( 𝐶 + 0 ) )
49 iftrue ⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = 𝐶 )
50 18 49 syl ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = 𝐶 )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = 𝐶 )
52 38 48 51 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
53 35 addid2d ⊢ ( 𝜑 → ( 0 + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → ( 0 + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
55 21 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
56 55 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( 0 + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
57 elun ⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
58 biorf ⊢ ( ¬ 𝑘 ∈ 𝐴 → ( 𝑘 ∈ 𝐵 ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) )
59 57 58 bitr4id ⊢ ( ¬ 𝑘 ∈ 𝐴 → ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑘 ∈ 𝐵 ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑘 ∈ 𝐵 ) )
61 60 ifbid ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
62 54 56 61 3eqtr4rd ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
63 52 62 pm2.61dan ⊢ ( 𝜑 → if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
64 63 sumeq2sdv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) = Σ 𝑘 ∈ 𝑍 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
65 4 unssad ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
66 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ )
67 sumss2 ⊢ ( ( ( 𝐴 ⊆ 𝑍 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
68 65 66 13 67 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
69 4 unssbd ⊢ ( 𝜑 → 𝐵 ⊆ 𝑍 )
70 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
71 sumss2 ⊢ ( ( ( 𝐵 ⊆ 𝑍 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ) ∧ ( 𝑍 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑍 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
72 69 70 13 71 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
73 68 72 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) = ( Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
74 37 64 73 3eqtr4rd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) = Σ 𝑘 ∈ 𝑍 if ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) , 𝐶 , 0 ) )
75 15 74 eqtr4d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )