# 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)

Ref Expression
Hypotheses fprodcnlem.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fprodcnlem.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
fprodcnlem.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
fprodcnlem.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodcnlem.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
fprodcnlem.z ${⊢}{\phi }\to {Z}\subseteq {A}$
fprodcnlem.w ${⊢}{\phi }\to {W}\in \left({A}\setminus {Z}\right)$
fprodcnlem.p ${⊢}{\phi }\to \left({x}\in {X}⟼\prod _{{k}\in {Z}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
Assertion fprodcnlem ${⊢}{\phi }\to \left({x}\in {X}⟼\prod _{{k}\in {Z}\cup \left\{{W}\right\}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$

### Proof

Step Hyp Ref Expression
1 fprodcnlem.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fprodcnlem.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 fprodcnlem.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
4 fprodcnlem.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 fprodcnlem.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
6 fprodcnlem.z ${⊢}{\phi }\to {Z}\subseteq {A}$
7 fprodcnlem.w ${⊢}{\phi }\to {W}\in \left({A}\setminus {Z}\right)$
8 fprodcnlem.p ${⊢}{\phi }\to \left({x}\in {X}⟼\prod _{{k}\in {Z}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
9 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{x}\in {X}$
10 1 9 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {X}\right)$
11 nfcsb1v
12 4 6 ssfid ${⊢}{\phi }\to {Z}\in \mathrm{Fin}$
13 12 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {Z}\in \mathrm{Fin}$
14 7 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {W}\in \left({A}\setminus {Z}\right)$
15 14 eldifbd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to ¬{W}\in {Z}$
16 6 sselda ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {k}\in {A}$
17 16 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {Z}\right)\to {k}\in {A}$
18 3 adantr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
19 2 cnfldtopon ${⊢}{K}\in \mathrm{TopOn}\left(ℂ\right)$
20 19 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {K}\in \mathrm{TopOn}\left(ℂ\right)$
21 cnf2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left(ℂ\right)\wedge \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)\right)\to \left({x}\in {X}⟼{B}\right):{X}⟶ℂ$
22 18 20 5 21 syl3anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right):{X}⟶ℂ$
23 eqid ${⊢}\left({x}\in {X}⟼{B}\right)=\left({x}\in {X}⟼{B}\right)$
24 23 fmpt ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℂ↔\left({x}\in {X}⟼{B}\right):{X}⟶ℂ$
25 22 24 sylibr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
26 25 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
27 simplr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {x}\in {X}$
28 rspa ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\wedge {x}\in {X}\right)\to {B}\in ℂ$
29 26 27 28 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
30 17 29 syldan ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {Z}\right)\to {B}\in ℂ$
31 csbeq1a
32 14 eldifad ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {W}\in {A}$
33 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {W}\in {A}\right)\to {W}\in {A}$
34 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{W}$
35 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{W}\in {A}$
36 10 35 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {W}\in {A}\right)$
37 11 nfel1
38 36 37 nfim
39 eleq1 ${⊢}{k}={W}\to \left({k}\in {A}↔{W}\in {A}\right)$
40 39 anbi2d ${⊢}{k}={W}\to \left(\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)↔\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {W}\in {A}\right)\right)$
41 31 eleq1d
42 40 41 imbi12d
43 34 38 42 29 vtoclgf
44 33 43 mpcom
45 32 44 mpdan
46 10 11 13 14 15 30 31 45 fprodsplitsn
47 46 mpteq2dva
48 7 eldifad ${⊢}{\phi }\to {W}\in {A}$
49 1 35 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {W}\in {A}\right)$
50 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{X}$
51 50 11 nfmpt
52 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({J}\mathrm{Cn}{K}\right)$
53 51 52 nfel
54 49 53 nfim
55 39 anbi2d ${⊢}{k}={W}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {W}\in {A}\right)\right)$
56 31 mpteq2dv
57 56 eleq1d
58 55 57 imbi12d
59 5 idi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
60 34 54 58 59 vtoclgf
61 60 anabsi7
62 48 61 mpdan
63 2 mulcn ${⊢}×\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
64 63 a1i ${⊢}{\phi }\to ×\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
65 3 8 62 64 cnmpt12f
66 47 65 eqeltrd ${⊢}{\phi }\to \left({x}\in {X}⟼\prod _{{k}\in {Z}\cup \left\{{W}\right\}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$