This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumclf

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

Ref Expression
Hypotheses fsumclf.ph 
|- F/ k ph
fsumclf.a 
|- ( ph -> A e. Fin )
fsumclf.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumclf 
|- ( ph -> sum_ k e. A B e. CC )

Proof

Step Hyp Ref Expression
1 fsumclf.ph 
 |-  F/ k ph
2 fsumclf.a 
 |-  ( ph -> A e. Fin )
3 fsumclf.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
5 nfcv 
 |-  F/_ j B
6 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
7 4 5 6 cbvsum 
 |-  sum_ k e. A B = sum_ j e. A [_ j / k ]_ B
8 7 a1i 
 |-  ( ph -> sum_ k e. A B = sum_ j e. A [_ j / k ]_ B )
9 nfv 
 |-  F/ k j e. A
10 1 9 nfan 
 |-  F/ k ( ph /\ j e. A )
11 6 nfel1 
 |-  F/ k [_ j / k ]_ B e. CC
12 10 11 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
13 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
14 13 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
15 4 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
16 14 15 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC ) ) )
17 12 16 3 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
18 2 17 fsumcl 
 |-  ( ph -> sum_ j e. A [_ j / k ]_ B e. CC )
19 8 18 eqeltrd 
 |-  ( ph -> sum_ k e. A B e. CC )