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 ( 𝜑 → Σ 𝑘 ∈ ( 𝐴𝐵 ) 𝐶 = ( Σ 𝑘𝐴 𝐶 + Σ 𝑘𝐵 𝐶 ) )