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	$$⊢Ⅎk\phi$$
	fsummulclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsummulclf.c	$$⊢\phi \to C\in ℂ$$
	fsummulclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	fsummulc1f	$$⊢\phi \to \sum _{k\in A}BC=\sum _{k\in A}BC$$

Proof

Step	Hyp	Ref	Expression
1		fsummulc1f.ph	$$⊢Ⅎk\phi$$
2		fsummulclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsummulclf.c	$$⊢\phi \to C\in ℂ$$
4		fsummulclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
5		csbeq1a	$$⊢k=j\to B=⦋j/k⦌B$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}jB$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌B$$
10	5 6 7 8 9	cbvsum	$$⊢\sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
11	10	oveq1i	$$⊢\sum _{k\in A}BC=\sum _{j\in A}⦋j/k⦌BC$$
12	11	a1i	$$⊢\phi \to \sum _{k\in A}BC=\sum _{j\in A}⦋j/k⦌BC$$
13		nfv	$$⊢Ⅎkj\in A$$
14	1 13	nfan	$$⊢Ⅎk\left(\phi \wedge j\in A\right)$$
15	9	nfel1	$$⊢Ⅎk⦋j/k⦌B\in ℂ$$
16	14 15	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ\right)$$
17		eleq1w	$$⊢k=j\to \left(k\in A\leftrightarrow j\in A\right)$$
18	17	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge j\in A\right)\right)$$
19	5	eleq1d	$$⊢k=j\to \left(B\in ℂ\leftrightarrow ⦋j/k⦌B\in ℂ\right)$$
20	18 19	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ\right)\right)$$
21	16 20 4	chvarfv	$$⊢\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ$$
22	2 3 21	fsummulc1	$$⊢\phi \to \sum _{j\in A}⦋j/k⦌BC=\sum _{j\in A}⦋j/k⦌BC$$
23		eqcom	$$⊢k=j\leftrightarrow j=k$$
24	23	imbi1i	$$⊢\left(k=j\to B=⦋j/k⦌B\right)\leftrightarrow \left(j=k\to B=⦋j/k⦌B\right)$$
25		eqcom	$$⊢B=⦋j/k⦌B\leftrightarrow ⦋j/k⦌B=B$$
26	25	imbi2i	$$⊢\left(j=k\to B=⦋j/k⦌B\right)\leftrightarrow \left(j=k\to ⦋j/k⦌B=B\right)$$
27	24 26	bitri	$$⊢\left(k=j\to B=⦋j/k⦌B\right)\leftrightarrow \left(j=k\to ⦋j/k⦌B=B\right)$$
28	5 27	mpbi	$$⊢j=k\to ⦋j/k⦌B=B$$
29	28	oveq1d	$$⊢j=k\to ⦋j/k⦌BC=BC$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}k\times$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}kC$$
32	9 30 31	nfov	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌BC$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}jBC$$
34	29 7 6 32 33	cbvsum	$$⊢\sum _{j\in A}⦋j/k⦌BC=\sum _{k\in A}BC$$
35	34	a1i	$$⊢\phi \to \sum _{j\in A}⦋j/k⦌BC=\sum _{k\in A}BC$$
36	12 22 35	3eqtrd	$$⊢\phi \to \sum _{k\in A}BC=\sum _{k\in A}BC$$