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 A
6		nfcv	|- F/_ k A
7		nfcv	|- F/_ j B
8		nfcsb1v	|- F/_ k [_ j / k ]_ B
9	4 5 6 7 8	cbvsum	|- sum_ k e. A B = sum_ j e. A [_ j / k ]_ B
10	9	a1i	|- ( ph -> sum_ k e. A B = sum_ j e. A [_ j / k ]_ B )
11		nfv	|- F/ k j e. A
12	1 11	nfan	|- F/ k ( ph /\ j e. A )
13	8	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	4	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 3	chvarfv	|- ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
20	2 19	fsumcl	|- ( ph -> sum_ j e. A [_ j / k ]_ B e. CC )
21	10 20	eqeltrd	|- ( ph -> sum_ k e. A B e. CC )