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 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
fsumsplit.2 ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
fsumsplit.3 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
fsumsplit.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
Assertion fsumsplit ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fsumsplit.1 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
2 fsumsplit.2 ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
3 fsumsplit.3 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
4 fsumsplit.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
5 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
6 5 2 sseqtrrid ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
7 6 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑈 )
8 7 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
9 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ )
10 3 olcd ⊢ ( 𝜑 → ( 𝑈 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝑈 ∈ Fin ) )
11 sumss2 ⊢ ( ( ( 𝐴 ⊆ 𝑈 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝑈 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝑈 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
12 6 9 10 11 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
13 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
14 13 2 sseqtrrid ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
15 14 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝑈 )
16 15 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
17 16 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
18 sumss2 ⊢ ( ( ( 𝐵 ⊆ 𝑈 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ) ∧ ( 𝑈 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝑈 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
19 14 17 10 18 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) )
20 12 19 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) = ( Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
21 0cn ⊢ 0 ∈ ℂ
22 ifcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
23 4 21 22 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℂ )
24 ifcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
25 4 21 24 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ∈ ℂ )
26 3 23 25 fsumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + Σ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) )
27 2 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) )
28 elun ⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
29 27 28 bitrdi ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) )
30 29 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
31 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
33 noel ⊢ ¬ 𝑘 ∈ ∅
34 1 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ↔ 𝑘 ∈ ∅ ) )
35 elin ⊢ ( 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
36 34 35 bitr3di ⊢ ( 𝜑 → ( 𝑘 ∈ ∅ ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
37 33 36 mtbii ⊢ ( 𝜑 → ¬ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
38 imnan ⊢ ( ( 𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵 ) ↔ ¬ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
39 37 38 sylibr ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵 ) )
40 39 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 ∈ 𝐵 )
41 40 iffalsed ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 0 )
42 32 41 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( 𝐶 + 0 ) )
43 8 addridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 + 0 ) = 𝐶 )
44 42 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = 𝐶 )
45 39 con2d ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴 ) )
46 45 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ¬ 𝑘 ∈ 𝐴 )
47 46 iffalsed ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
48 iftrue ⊢ ( 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 𝐶 )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) = 𝐶 )
50 47 49 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = ( 0 + 𝐶 ) )
51 16 addlidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 0 + 𝐶 ) = 𝐶 )
52 50 51 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = 𝐶 )
53 44 52 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = 𝐶 )
54 30 53 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = 𝐶 )
55 54 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) + if ( 𝑘 ∈ 𝐵 , 𝐶 , 0 ) ) = Σ 𝑘 ∈ 𝑈 𝐶 )
56 20 26 55 3eqtr2rd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑈 𝐶 = ( Σ 𝑘 ∈ 𝐴 𝐶 + Σ 𝑘 ∈ 𝐵 𝐶 ) )