Metamath Proof Explorer


Theorem fprodcnlem

Description: A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

Ref Expression
Hypotheses fprodcnlem.1 k φ
fprodcnlem.k K = TopOpen fld
fprodcnlem.j φ J TopOn X
fprodcnlem.a φ A Fin
fprodcnlem.b φ k A x X B J Cn K
fprodcnlem.z φ Z A
fprodcnlem.w φ W A Z
fprodcnlem.p φ x X k Z B J Cn K
Assertion fprodcnlem φ x X k Z W B J Cn K

Proof

Step Hyp Ref Expression
1 fprodcnlem.1 k φ
2 fprodcnlem.k K = TopOpen fld
3 fprodcnlem.j φ J TopOn X
4 fprodcnlem.a φ A Fin
5 fprodcnlem.b φ k A x X B J Cn K
6 fprodcnlem.z φ Z A
7 fprodcnlem.w φ W A Z
8 fprodcnlem.p φ x X k Z B J Cn K
9 nfv k x X
10 1 9 nfan k φ x X
11 nfcsb1v _ k W / k B
12 4 6 ssfid φ Z Fin
13 12 adantr φ x X Z Fin
14 7 adantr φ x X W A Z
15 14 eldifbd φ x X ¬ W Z
16 6 sselda φ k Z k A
17 16 adantlr φ x X k Z k A
18 3 adantr φ k A J TopOn X
19 2 cnfldtopon K TopOn
20 19 a1i φ k A K TopOn
21 cnf2 J TopOn X K TopOn x X B J Cn K x X B : X
22 18 20 5 21 syl3anc φ k A x X B : X
23 eqid x X B = x X B
24 23 fmpt x X B x X B : X
25 22 24 sylibr φ k A x X B
26 25 adantlr φ x X k A x X B
27 simplr φ x X k A x X
28 rspa x X B x X B
29 26 27 28 syl2anc φ x X k A B
30 17 29 syldan φ x X k Z B
31 csbeq1a k = W B = W / k B
32 14 eldifad φ x X W A
33 nfv k W A
34 10 33 nfan k φ x X W A
35 11 nfel1 k W / k B
36 34 35 nfim k φ x X W A W / k B
37 eleq1 k = W k A W A
38 37 anbi2d k = W φ x X k A φ x X W A
39 31 eleq1d k = W B W / k B
40 38 39 imbi12d k = W φ x X k A B φ x X W A W / k B
41 36 40 29 vtoclg1f W A φ x X W A W / k B
42 41 anabsi7 φ x X W A W / k B
43 32 42 mpdan φ x X W / k B
44 10 11 13 14 15 30 31 43 fprodsplitsn φ x X k Z W B = k Z B W / k B
45 44 mpteq2dva φ x X k Z W B = x X k Z B W / k B
46 7 eldifad φ W A
47 1 33 nfan k φ W A
48 nfcv _ k X
49 48 11 nfmpt _ k x X W / k B
50 49 nfel1 k x X W / k B J Cn K
51 47 50 nfim k φ W A x X W / k B J Cn K
52 37 anbi2d k = W φ k A φ W A
53 31 mpteq2dv k = W x X B = x X W / k B
54 53 eleq1d k = W x X B J Cn K x X W / k B J Cn K
55 52 54 imbi12d k = W φ k A x X B J Cn K φ W A x X W / k B J Cn K
56 51 55 5 vtoclg1f W A φ W A x X W / k B J Cn K
57 56 anabsi7 φ W A x X W / k B J Cn K
58 46 57 mpdan φ x X W / k B J Cn K
59 19 a1i φ K TopOn
60 2 mpomulcn u , v u v K × t K Cn K
61 60 a1i φ u , v u v K × t K Cn K
62 oveq12 u = k Z B v = W / k B u v = k Z B W / k B
63 3 8 58 59 59 61 62 cnmpt12 φ x X k Z B W / k B J Cn K
64 45 63 eqeltrd φ x X k Z W B J Cn K