# 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 )`
` |-  ( ( 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 )`
` |-  ( ph -> ( sum_ k e. ( A \ { C } ) B + D ) = ( D + sum_ k e. ( A \ { C } ) B ) )`
` |-  ( ph -> sum_ k e. A B = ( D + sum_ k e. ( A \ { C } ) B ) )`