Metamath Proof Explorer

Theorem fsumsplit1

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

Ref Expression
Hypotheses fsumsplit1.kph 
|- F/ k ph
fsumsplit1.kd 
|- F/_ k D
fsumsplit1.a 
|- ( ph -> A e. Fin )
fsumsplit1.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fsumsplit1.c 
|- ( ph -> C e. A )
fsumsplit1.bd 
|- ( k = C -> B = D )
Assertion fsumsplit1 
|- ( ph -> sum_ k e. A B = ( D + sum_ k e. ( A \ { C } ) B ) )

Proof

Step Hyp Ref Expression
1 fsumsplit1.kph 
 |-  F/ k ph
2 fsumsplit1.kd 
 |-  F/_ k D
3 fsumsplit1.a 
 |-  ( ph -> A e. Fin )
4 fsumsplit1.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 fsumsplit1.c 
 |-  ( ph -> C e. A )
6 fsumsplit1.bd 
 |-  ( k = C -> B = D )
7 uncom 
 |-  ( ( A \ { C } ) u. { C } ) = ( { C } u. ( A \ { C } ) )
8 7 a1i 
 |-  ( ph -> ( ( A \ { C } ) u. { C } ) = ( { C } u. ( A \ { C } ) ) )
9 5 snssd 
 |-  ( ph -> { C } C_ A )
10 undif 
 |-  ( { C } C_ A <-> ( { C } u. ( A \ { C } ) ) = A )
11 9 10 sylib 
 |-  ( ph -> ( { C } u. ( A \ { C } ) ) = A )
12 eqidd 
 |-  ( ph -> A = A )
13 8 11 12 3eqtrrd 
 |-  ( ph -> A = ( ( A \ { C } ) u. { C } ) )
14 13 sumeq1d 
 |-  ( ph -> sum_ k e. A B = sum_ k e. ( ( A \ { C } ) u. { C } ) B )
15 diffi 
 |-  ( A e. Fin -> ( A \ { C } ) e. Fin )
16 3 15 syl 
 |-  ( ph -> ( A \ { C } ) e. Fin )
17 neldifsnd 
 |-  ( ph -> -. C e. ( A \ { C } ) )
18 simpl 
 |-  ( ( ph /\ k e. ( A \ { C } ) ) -> ph )
19 eldifi 
 |-  ( k e. ( A \ { C } ) -> k e. A )
20 19 adantl 
 |-  ( ( ph /\ k e. ( A \ { C } ) ) -> k e. A )
21 18 20 4 syl2anc 
 |-  ( ( ph /\ k e. ( A \ { C } ) ) -> B e. CC )
22 2 a1i 
 |-  ( ph -> F/_ k D )
23 simpr 
 |-  ( ( ph /\ k = C ) -> k = C )
24 23 6 syl 
 |-  ( ( ph /\ k = C ) -> B = D )
25 1 22 5 24 csbiedf 
 |-  ( ph -> [_ C / k ]_ B = D )
26 25 eqcomd 
 |-  ( ph -> D = [_ C / k ]_ B )
27 5 ancli 
 |-  ( ph -> ( ph /\ C e. A ) )
28 nfcv 
 |-  F/_ k C
29 nfv 
 |-  F/ k C e. A
30 1 29 nfan 
 |-  F/ k ( ph /\ C e. A )
31 28 nfcsb1 
 |-  F/_ k [_ C / k ]_ B
32 nfcv 
 |-  F/_ k CC
33 31 32 nfel 
 |-  F/ k [_ C / k ]_ B e. CC
34 30 33 nfim 
 |-  F/ k ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC )
35 eleq1 
 |-  ( k = C -> ( k e. A <-> C e. A ) )
36 35 anbi2d 
 |-  ( k = C -> ( ( ph /\ k e. A ) <-> ( ph /\ C e. A ) ) )
37 csbeq1a 
 |-  ( k = C -> B = [_ C / k ]_ B )
38 37 eleq1d 
 |-  ( k = C -> ( B e. CC <-> [_ C / k ]_ B e. CC ) )
39 36 38 imbi12d 
 |-  ( k = C -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC ) ) )
40 28 34 39 4 vtoclgf 
 |-  ( C e. A -> ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC ) )
41 5 27 40 sylc 
 |-  ( ph -> [_ C / k ]_ B e. CC )
42 26 41 eqeltrd 
 |-  ( ph -> D e. CC )
43 1 2 16 5 17 21 6 42 fsumsplitsn 
 |-  ( ph -> sum_ k e. ( ( A \ { C } ) u. { C } ) B = ( sum_ k e. ( A \ { C } ) B + D ) )
44 1 16 21 fsumclf 
 |-  ( ph -> sum_ k e. ( A \ { C } ) B e. CC )
45 44 42 addcomd 
 |-  ( ph -> ( sum_ k e. ( A \ { C } ) B + D ) = ( D + sum_ k e. ( A \ { C } ) B ) )
46 14 43 45 3eqtrd 
 |-  ( ph -> sum_ k e. A B = ( D + sum_ k e. ( A \ { C } ) B ) )