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