Metamath Proof Explorer

Theorem fsumsplitsndif

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsumsplitsndif 
|- ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ k e. A B = ( sum_ k e. ( A \ { X } ) B + [_ X / k ]_ B ) )

Proof

Step Hyp Ref Expression
1 neldifsnd 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> -. X e. ( A \ { X } ) )
2 disjsn 
 |-  ( ( ( A \ { X } ) i^i { X } ) = (/) <-> -. X e. ( A \ { X } ) )
3 1 2 sylibr 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> ( ( A \ { X } ) i^i { X } ) = (/) )
4 uncom 
 |-  ( ( A \ { X } ) u. { X } ) = ( { X } u. ( A \ { X } ) )
5 simp2 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> X e. A )
6 5 snssd 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> { X } C_ A )
7 undif 
 |-  ( { X } C_ A <-> ( { X } u. ( A \ { X } ) ) = A )
8 6 7 sylib 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> ( { X } u. ( A \ { X } ) ) = A )
9 4 8 syl5req 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> A = ( ( A \ { X } ) u. { X } ) )
10 simp1 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> A e. Fin )
11 rspcsbela 
 |-  ( ( x e. A /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
12 11 zcnd 
 |-  ( ( x e. A /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. CC )
13 12 expcom 
 |-  ( A. k e. A B e. ZZ -> ( x e. A -> [_ x / k ]_ B e. CC ) )
14 13 3ad2ant3 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> ( x e. A -> [_ x / k ]_ B e. CC ) )
15 14 imp 
 |-  ( ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) /\ x e. A ) -> [_ x / k ]_ B e. CC )
16 3 9 10 15 fsumsplit 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ x e. A [_ x / k ]_ B = ( sum_ x e. ( A \ { X } ) [_ x / k ]_ B + sum_ x e. { X } [_ x / k ]_ B ) )
17 nfcv 
 |-  F/_ x B
18 nfcsb1v 
 |-  F/_ k [_ x / k ]_ B
19 csbeq1a 
 |-  ( k = x -> B = [_ x / k ]_ B )
20 17 18 19 cbvsumi 
 |-  sum_ k e. A B = sum_ x e. A [_ x / k ]_ B
21 17 18 19 cbvsumi 
 |-  sum_ k e. ( A \ { X } ) B = sum_ x e. ( A \ { X } ) [_ x / k ]_ B
22 17 18 19 cbvsumi 
 |-  sum_ k e. { X } B = sum_ x e. { X } [_ x / k ]_ B
23 21 22 oveq12i 
 |-  ( sum_ k e. ( A \ { X } ) B + sum_ k e. { X } B ) = ( sum_ x e. ( A \ { X } ) [_ x / k ]_ B + sum_ x e. { X } [_ x / k ]_ B )
24 16 20 23 3eqtr4g 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ k e. A B = ( sum_ k e. ( A \ { X } ) B + sum_ k e. { X } B ) )
25 rspcsbela 
 |-  ( ( X e. A /\ A. k e. A B e. ZZ ) -> [_ X / k ]_ B e. ZZ )
26 25 zcnd 
 |-  ( ( X e. A /\ A. k e. A B e. ZZ ) -> [_ X / k ]_ B e. CC )
27 26 3adant1 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> [_ X / k ]_ B e. CC )
28 sumsns 
 |-  ( ( X e. A /\ [_ X / k ]_ B e. CC ) -> sum_ k e. { X } B = [_ X / k ]_ B )
29 5 27 28 syl2anc 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ k e. { X } B = [_ X / k ]_ B )
30 29 oveq2d 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> ( sum_ k e. ( A \ { X } ) B + sum_ k e. { X } B ) = ( sum_ k e. ( A \ { X } ) B + [_ X / k ]_ B ) )
31 24 30 eqtrd 
 |-  ( ( A e. Fin /\ X e. A /\ A. k e. A B e. ZZ ) -> sum_ k e. A B = ( sum_ k e. ( A \ { X } ) B + [_ X / k ]_ B ) )