Metamath Proof Explorer

Theorem fsumsplitsn

Description: Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumsplitsn.ph 
|- F/ k ph
fsumsplitsn.kd 
|- F/_ k D
fsumsplitsn.a 
|- ( ph -> A e. Fin )
fsumsplitsn.b 
|- ( ph -> B e. V )
fsumsplitsn.ba 
|- ( ph -> -. B e. A )
fsumsplitsn.c 
|- ( ( ph /\ k e. A ) -> C e. CC )
fsumsplitsn.d 
|- ( k = B -> C = D )
fsumsplitsn.dcn 
|- ( ph -> D e. CC )
Assertion fsumsplitsn 
|- ( ph -> sum_ k e. ( A u. { B } ) C = ( sum_ k e. A C + D ) )

Proof

Step Hyp Ref Expression
1 fsumsplitsn.ph 
 |-  F/ k ph
2 fsumsplitsn.kd 
 |-  F/_ k D
3 fsumsplitsn.a 
 |-  ( ph -> A e. Fin )
4 fsumsplitsn.b 
 |-  ( ph -> B e. V )
5 fsumsplitsn.ba 
 |-  ( ph -> -. B e. A )
6 fsumsplitsn.c 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
7 fsumsplitsn.d 
 |-  ( k = B -> C = D )
8 fsumsplitsn.dcn 
 |-  ( ph -> D e. CC )
9 disjsn 
 |-  ( ( A i^i { B } ) = (/) <-> -. B e. A )
10 5 9 sylibr 
 |-  ( ph -> ( A i^i { B } ) = (/) )
11 eqidd 
 |-  ( ph -> ( A u. { B } ) = ( A u. { B } ) )
12 snfi 
 |-  { B } e. Fin
13 unfi 
 |-  ( ( A e. Fin /\ { B } e. Fin ) -> ( A u. { B } ) e. Fin )
14 3 12 13 sylancl 
 |-  ( ph -> ( A u. { B } ) e. Fin )
15 6 adantlr 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ k e. A ) -> C e. CC )
16 simpll 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> ph )
17 elunnel1 
 |-  ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k e. { B } )
18 elsni 
 |-  ( k e. { B } -> k = B )
19 17 18 syl 
 |-  ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k = B )
20 19 adantll 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> k = B )
21 7 adantl 
 |-  ( ( ph /\ k = B ) -> C = D )
22 8 adantr 
 |-  ( ( ph /\ k = B ) -> D e. CC )
23 21 22 eqeltrd 
 |-  ( ( ph /\ k = B ) -> C e. CC )
24 16 20 23 syl2anc 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> C e. CC )
25 15 24 pm2.61dan 
 |-  ( ( ph /\ k e. ( A u. { B } ) ) -> C e. CC )
26 1 10 11 14 25 fsumsplitf 
 |-  ( ph -> sum_ k e. ( A u. { B } ) C = ( sum_ k e. A C + sum_ k e. { B } C ) )
27 2 7 sumsnf 
 |-  ( ( B e. V /\ D e. CC ) -> sum_ k e. { B } C = D )
28 4 8 27 syl2anc 
 |-  ( ph -> sum_ k e. { B } C = D )
29 28 oveq2d 
 |-  ( ph -> ( sum_ k e. A C + sum_ k e. { B } C ) = ( sum_ k e. A C + D ) )
30 26 29 eqtrd 
 |-  ( ph -> sum_ k e. ( A u. { B } ) C = ( sum_ k e. A C + D ) )