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 φ A B =
fsumsplit.2 φ U = A B
fsumsplit.3 φ U Fin
fsumsplit.4 φ k U C
Assertion fsumsplit φ k U C = k A C + k B C

Proof

Step Hyp Ref Expression
1 fsumsplit.1 φ A B =
2 fsumsplit.2 φ U = A B
3 fsumsplit.3 φ U Fin
4 fsumsplit.4 φ k U C
5 ssun1 A A B
6 5 2 sseqtrrid φ A U
7 6 sselda φ k A k U
8 7 4 syldan φ k A C
9 8 ralrimiva φ k A C
10 3 olcd φ U 0 U Fin
11 sumss2 A U k A C U 0 U Fin k A C = k U if k A C 0
12 6 9 10 11 syl21anc φ k A C = k U if k A C 0
13 ssun2 B A B
14 13 2 sseqtrrid φ B U
15 14 sselda φ k B k U
16 15 4 syldan φ k B C
17 16 ralrimiva φ k B C
18 sumss2 B U k B C U 0 U Fin k B C = k U if k B C 0
19 14 17 10 18 syl21anc φ k B C = k U if k B C 0
20 12 19 oveq12d φ k A C + k B C = k U if k A C 0 + k U if k B C 0
21 0cn 0
22 ifcl C 0 if k A C 0
23 4 21 22 sylancl φ k U if k A C 0
24 ifcl C 0 if k B C 0
25 4 21 24 sylancl φ k U if k B C 0
26 3 23 25 fsumadd φ k U if k A C 0 + if k B C 0 = k U if k A C 0 + k U if k B C 0
27 2 eleq2d φ k U k A B
28 elun k A B k A k B
29 27 28 syl6bb φ k U k A k B
30 29 biimpa φ k U k A k B
31 iftrue k A if k A C 0 = C
32 31 adantl φ k A if k A C 0 = C
33 noel ¬ k
34 elin k A B k A k B
35 1 eleq2d φ k A B k
36 34 35 syl5rbbr φ k k A k B
37 33 36 mtbii φ ¬ k A k B
38 imnan k A ¬ k B ¬ k A k B
39 37 38 sylibr φ k A ¬ k B
40 39 imp φ k A ¬ k B
41 40 iffalsed φ k A if k B C 0 = 0
42 32 41 oveq12d φ k A if k A C 0 + if k B C 0 = C + 0
43 8 addid1d φ k A C + 0 = C
44 42 43 eqtrd φ k A if k A C 0 + if k B C 0 = C
45 39 con2d φ k B ¬ k A
46 45 imp φ k B ¬ k A
47 46 iffalsed φ k B if k A C 0 = 0
48 iftrue k B if k B C 0 = C
49 48 adantl φ k B if k B C 0 = C
50 47 49 oveq12d φ k B if k A C 0 + if k B C 0 = 0 + C
51 16 addid2d φ k B 0 + C = C
52 50 51 eqtrd φ k B if k A C 0 + if k B C 0 = C
53 44 52 jaodan φ k A k B if k A C 0 + if k B C 0 = C
54 30 53 syldan φ k U if k A C 0 + if k B C 0 = C
55 54 sumeq2dv φ k U if k A C 0 + if k B C 0 = k U C
56 20 26 55 3eqtr2rd φ k U C = k A C + k B C