Metamath Proof Explorer

Theorem fsumsplitsnun

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 17-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( Z e/ A <-> -. Z e. A )
2 disjsn 
 |-  ( ( A i^i { Z } ) = (/) <-> -. Z e. A )
3 1 2 sylbb2 
 |-  ( Z e/ A -> ( A i^i { Z } ) = (/) )
4 3 adantl 
 |-  ( ( Z e. V /\ Z e/ A ) -> ( A i^i { Z } ) = (/) )
5 4 3ad2ant2 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( A i^i { Z } ) = (/) )
6 eqidd 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( A u. { Z } ) = ( A u. { Z } ) )
7 snfi 
 |-  { Z } e. Fin
8 unfi 
 |-  ( ( A e. Fin /\ { Z } e. Fin ) -> ( A u. { Z } ) e. Fin )
9 7 8 mpan2 
 |-  ( A e. Fin -> ( A u. { Z } ) e. Fin )
10 9 3ad2ant1 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( A u. { Z } ) e. Fin )
11 rspcsbela 
 |-  ( ( x e. ( A u. { Z } ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
12 11 expcom 
 |-  ( A. k e. ( A u. { Z } ) B e. ZZ -> ( x e. ( A u. { Z } ) -> [_ x / k ]_ B e. ZZ ) )
13 12 3ad2ant3 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( x e. ( A u. { Z } ) -> [_ x / k ]_ B e. ZZ ) )
14 13 imp 
 |-  ( ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) /\ x e. ( A u. { Z } ) ) -> [_ x / k ]_ B e. ZZ )
15 14 zcnd 
 |-  ( ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) /\ x e. ( A u. { Z } ) ) -> [_ x / k ]_ B e. CC )
16 5 6 10 15 fsumsplit 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ x e. ( A u. { Z } ) [_ x / k ]_ B = ( sum_ x e. A [_ x / k ]_ B + sum_ x e. { Z } [_ x / k ]_ B ) )
17 csbeq1a 
 |-  ( k = x -> B = [_ x / k ]_ B )
18 nfcv 
 |-  F/_ x B
19 nfcsb1v 
 |-  F/_ k [_ x / k ]_ B
20 17 18 19 cbvsum 
 |-  sum_ k e. ( A u. { Z } ) B = sum_ x e. ( A u. { Z } ) [_ x / k ]_ B
21 17 18 19 cbvsum 
 |-  sum_ k e. A B = sum_ x e. A [_ x / k ]_ B
22 17 18 19 cbvsum 
 |-  sum_ k e. { Z } B = sum_ x e. { Z } [_ x / k ]_ B
23 21 22 oveq12i 
 |-  ( sum_ k e. A B + sum_ k e. { Z } B ) = ( sum_ x e. A [_ x / k ]_ B + sum_ x e. { Z } [_ x / k ]_ B )
24 16 20 23 3eqtr4g 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. ( A u. { Z } ) B = ( sum_ k e. A B + sum_ k e. { Z } B ) )
25 simp2l 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> Z e. V )
26 snidg 
 |-  ( Z e. V -> Z e. { Z } )
27 26 adantr 
 |-  ( ( Z e. V /\ Z e/ A ) -> Z e. { Z } )
28 27 3ad2ant2 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> Z e. { Z } )
29 elun2 
 |-  ( Z e. { Z } -> Z e. ( A u. { Z } ) )
30 28 29 syl 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> Z e. ( A u. { Z } ) )
31 simp3 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> A. k e. ( A u. { Z } ) B e. ZZ )
32 rspcsbela 
 |-  ( ( Z e. ( A u. { Z } ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> [_ Z / k ]_ B e. ZZ )
33 30 31 32 syl2anc 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> [_ Z / k ]_ B e. ZZ )
34 33 zcnd 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> [_ Z / k ]_ B e. CC )
35 sumsns 
 |-  ( ( Z e. V /\ [_ Z / k ]_ B e. CC ) -> sum_ k e. { Z } B = [_ Z / k ]_ B )
36 25 34 35 syl2anc 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. { Z } B = [_ Z / k ]_ B )
37 36 oveq2d 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( sum_ k e. A B + sum_ k e. { Z } B ) = ( sum_ k e. A B + [_ Z / k ]_ B ) )
38 24 37 eqtrd 
 |-  ( ( A e. Fin /\ ( Z e. V /\ Z e/ A ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. ( A u. { Z } ) B = ( sum_ k e. A B + [_ Z / k ]_ B ) )