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 𝑘 𝜑
fprodcnlem.k 𝐾 = ( TopOpen ‘ ℂfld )
fprodcnlem.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
fprodcnlem.a ( 𝜑𝐴 ∈ Fin )
fprodcnlem.b ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
fprodcnlem.z ( 𝜑𝑍𝐴 )
fprodcnlem.w ( 𝜑𝑊 ∈ ( 𝐴𝑍 ) )
fprodcnlem.p ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑘𝑍 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion fprodcnlem ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fprodcnlem.1 𝑘 𝜑
2 fprodcnlem.k 𝐾 = ( TopOpen ‘ ℂfld )
3 fprodcnlem.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 fprodcnlem.a ( 𝜑𝐴 ∈ Fin )
5 fprodcnlem.b ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
6 fprodcnlem.z ( 𝜑𝑍𝐴 )
7 fprodcnlem.w ( 𝜑𝑊 ∈ ( 𝐴𝑍 ) )
8 fprodcnlem.p ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑘𝑍 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
9 nfv 𝑘 𝑥𝑋
10 1 9 nfan 𝑘 ( 𝜑𝑥𝑋 )
11 nfcsb1v 𝑘 𝑊 / 𝑘 𝐵
12 4 6 ssfid ( 𝜑𝑍 ∈ Fin )
13 12 adantr ( ( 𝜑𝑥𝑋 ) → 𝑍 ∈ Fin )
14 7 adantr ( ( 𝜑𝑥𝑋 ) → 𝑊 ∈ ( 𝐴𝑍 ) )
15 14 eldifbd ( ( 𝜑𝑥𝑋 ) → ¬ 𝑊𝑍 )
16 6 sselda ( ( 𝜑𝑘𝑍 ) → 𝑘𝐴 )
17 16 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝑍 ) → 𝑘𝐴 )
18 3 adantr ( ( 𝜑𝑘𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 2 cnfldtopon 𝐾 ∈ ( TopOn ‘ ℂ )
20 19 a1i ( ( 𝜑𝑘𝐴 ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
21 cnf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝑥𝑋𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥𝑋𝐵 ) : 𝑋 ⟶ ℂ )
22 18 20 5 21 syl3anc ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋𝐵 ) : 𝑋 ⟶ ℂ )
23 eqid ( 𝑥𝑋𝐵 ) = ( 𝑥𝑋𝐵 )
24 23 fmpt ( ∀ 𝑥𝑋 𝐵 ∈ ℂ ↔ ( 𝑥𝑋𝐵 ) : 𝑋 ⟶ ℂ )
25 22 24 sylibr ( ( 𝜑𝑘𝐴 ) → ∀ 𝑥𝑋 𝐵 ∈ ℂ )
26 25 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝐴 ) → ∀ 𝑥𝑋 𝐵 ∈ ℂ )
27 simplr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝐴 ) → 𝑥𝑋 )
28 rspa ( ( ∀ 𝑥𝑋 𝐵 ∈ ℂ ∧ 𝑥𝑋 ) → 𝐵 ∈ ℂ )
29 26 27 28 syl2anc ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ )
30 17 29 syldan ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝑍 ) → 𝐵 ∈ ℂ )
31 csbeq1a ( 𝑘 = 𝑊𝐵 = 𝑊 / 𝑘 𝐵 )
32 14 eldifad ( ( 𝜑𝑥𝑋 ) → 𝑊𝐴 )
33 nfv 𝑘 𝑊𝐴
34 10 33 nfan 𝑘 ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 )
35 11 nfel1 𝑘 𝑊 / 𝑘 𝐵 ∈ ℂ
36 34 35 nfim 𝑘 ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 ) → 𝑊 / 𝑘 𝐵 ∈ ℂ )
37 eleq1 ( 𝑘 = 𝑊 → ( 𝑘𝐴𝑊𝐴 ) )
38 37 anbi2d ( 𝑘 = 𝑊 → ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝐴 ) ↔ ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 ) ) )
39 31 eleq1d ( 𝑘 = 𝑊 → ( 𝐵 ∈ ℂ ↔ 𝑊 / 𝑘 𝐵 ∈ ℂ ) )
40 38 39 imbi12d ( 𝑘 = 𝑊 → ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 ) → 𝑊 / 𝑘 𝐵 ∈ ℂ ) ) )
41 36 40 29 vtoclg1f ( 𝑊𝐴 → ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 ) → 𝑊 / 𝑘 𝐵 ∈ ℂ ) )
42 41 anabsi7 ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑊𝐴 ) → 𝑊 / 𝑘 𝐵 ∈ ℂ )
43 32 42 mpdan ( ( 𝜑𝑥𝑋 ) → 𝑊 / 𝑘 𝐵 ∈ ℂ )
44 10 11 13 14 15 30 31 43 fprodsplitsn ( ( 𝜑𝑥𝑋 ) → ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 = ( ∏ 𝑘𝑍 𝐵 · 𝑊 / 𝑘 𝐵 ) )
45 44 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) = ( 𝑥𝑋 ↦ ( ∏ 𝑘𝑍 𝐵 · 𝑊 / 𝑘 𝐵 ) ) )
46 7 eldifad ( 𝜑𝑊𝐴 )
47 1 33 nfan 𝑘 ( 𝜑𝑊𝐴 )
48 nfcv 𝑘 𝑋
49 48 11 nfmpt 𝑘 ( 𝑥𝑋 𝑊 / 𝑘 𝐵 )
50 49 nfel1 𝑘 ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 )
51 47 50 nfim 𝑘 ( ( 𝜑𝑊𝐴 ) → ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
52 37 anbi2d ( 𝑘 = 𝑊 → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑𝑊𝐴 ) ) )
53 31 mpteq2dv ( 𝑘 = 𝑊 → ( 𝑥𝑋𝐵 ) = ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) )
54 53 eleq1d ( 𝑘 = 𝑊 → ( ( 𝑥𝑋𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
55 52 54 imbi12d ( 𝑘 = 𝑊 → ( ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ↔ ( ( 𝜑𝑊𝐴 ) → ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) ) )
56 51 55 5 vtoclg1f ( 𝑊𝐴 → ( ( 𝜑𝑊𝐴 ) → ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
57 56 anabsi7 ( ( 𝜑𝑊𝐴 ) → ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
58 46 57 mpdan ( 𝜑 → ( 𝑥𝑋 𝑊 / 𝑘 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
59 19 a1i ( 𝜑𝐾 ∈ ( TopOn ‘ ℂ ) )
60 2 mpomulcn ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
61 60 a1i ( 𝜑 → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
62 oveq12 ( ( 𝑢 = ∏ 𝑘𝑍 𝐵𝑣 = 𝑊 / 𝑘 𝐵 ) → ( 𝑢 · 𝑣 ) = ( ∏ 𝑘𝑍 𝐵 · 𝑊 / 𝑘 𝐵 ) )
63 3 8 58 59 59 61 62 cnmpt12 ( 𝜑 → ( 𝑥𝑋 ↦ ( ∏ 𝑘𝑍 𝐵 · 𝑊 / 𝑘 𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
64 45 63 eqeltrd ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑘 ∈ ( 𝑍 ∪ { 𝑊 } ) 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )