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