Metamath Proof Explorer

Theorem fsummulc1f

Description: Closure of a finite sum of complex numbers A ( k ) . A version of fsummulc1 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsummulc1f.ph 
|- F/ k ph
fsummulclf.a 
|- ( ph -> A e. Fin )
fsummulclf.c 
|- ( ph -> C e. CC )
fsummulclf.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsummulc1f 
|- ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )

Proof

Step Hyp Ref Expression
1 fsummulc1f.ph 
 |-  F/ k ph
2 fsummulclf.a 
 |-  ( ph -> A e. Fin )
3 fsummulclf.c 
 |-  ( ph -> C e. CC )
4 fsummulclf.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
6 nfcv 
 |-  F/_ j A
7 nfcv 
 |-  F/_ k A
8 nfcv 
 |-  F/_ j B
9 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
10 5 6 7 8 9 cbvsum 
 |-  sum_ k e. A B = sum_ j e. A [_ j / k ]_ B
11 10 oveq1i 
 |-  ( sum_ k e. A B x. C ) = ( sum_ j e. A [_ j / k ]_ B x. C )
12 11 a1i 
 |-  ( ph -> ( sum_ k e. A B x. C ) = ( sum_ j e. A [_ j / k ]_ B x. C ) )
13 nfv 
 |-  F/ k j e. A
14 1 13 nfan 
 |-  F/ k ( ph /\ j e. A )
15 9 nfel1 
 |-  F/ k [_ j / k ]_ B e. CC
16 14 15 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
17 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
18 17 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
19 5 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
20 18 19 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC ) ) )
21 16 20 4 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
22 2 3 21 fsummulc1 
 |-  ( ph -> ( sum_ j e. A [_ j / k ]_ B x. C ) = sum_ j e. A ( [_ j / k ]_ B x. C ) )
23 eqcom 
 |-  ( k = j <-> j = k )
24 23 imbi1i 
 |-  ( ( k = j -> B = [_ j / k ]_ B ) <-> ( j = k -> B = [_ j / k ]_ B ) )
25 eqcom 
 |-  ( B = [_ j / k ]_ B <-> [_ j / k ]_ B = B )
26 25 imbi2i 
 |-  ( ( j = k -> B = [_ j / k ]_ B ) <-> ( j = k -> [_ j / k ]_ B = B ) )
27 24 26 bitri 
 |-  ( ( k = j -> B = [_ j / k ]_ B ) <-> ( j = k -> [_ j / k ]_ B = B ) )
28 5 27 mpbi 
 |-  ( j = k -> [_ j / k ]_ B = B )
29 28 oveq1d 
 |-  ( j = k -> ( [_ j / k ]_ B x. C ) = ( B x. C ) )
30 nfcv 
 |-  F/_ k x.
31 nfcv 
 |-  F/_ k C
32 9 30 31 nfov 
 |-  F/_ k ( [_ j / k ]_ B x. C )
33 nfcv 
 |-  F/_ j ( B x. C )
34 29 7 6 32 33 cbvsum 
 |-  sum_ j e. A ( [_ j / k ]_ B x. C ) = sum_ k e. A ( B x. C )
35 34 a1i 
 |-  ( ph -> sum_ j e. A ( [_ j / k ]_ B x. C ) = sum_ k e. A ( B x. C ) )
36 12 22 35 3eqtrd 
 |-  ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )