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 k φ
fsummulclf.a φ A Fin
fsummulclf.c φ C
fsummulclf.b φ k A B
Assertion fsummulc1f φ k A B C = k A B C

Proof

Step Hyp Ref Expression
1 fsummulc1f.ph k φ
2 fsummulclf.a φ A Fin
3 fsummulclf.c φ C
4 fsummulclf.b φ k A B
5 csbeq1a k = j B = j / k B
6 nfcv _ j A
7 nfcv _ k A
8 nfcv _ j B
9 nfcsb1v _ k j / k B
10 5 6 7 8 9 cbvsum k A B = j A j / k B
11 10 oveq1i k A B C = j A j / k B C
12 11 a1i φ k A B C = j A j / k B C
13 nfv k j A
14 1 13 nfan k φ j A
15 9 nfel1 k j / k B
16 14 15 nfim k φ j A j / k B
17 eleq1w k = j k A j A
18 17 anbi2d k = j φ k A φ j A
19 5 eleq1d k = j B j / k B
20 18 19 imbi12d k = j φ k A B φ j A j / k B
21 16 20 4 chvarfv φ j A j / k B
22 2 3 21 fsummulc1 φ j A j / k B C = j A j / k B 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 C = B C
30 nfcv _ k ×
31 nfcv _ k C
32 9 30 31 nfov _ k j / k B C
33 nfcv _ j B C
34 29 7 6 32 33 cbvsum j A j / k B C = k A B C
35 34 a1i φ j A j / k B C = k A B C
36 12 22 35 3eqtrd φ k A B C = k A B C