Metamath Proof Explorer


Theorem fprodsub2cncf

Description: F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodsub2cncf.k 𝑘 𝜑
fprodsub2cncf.a ( 𝜑𝐴 ∈ Fin )
fprodsub2cncf.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
fprodsub2cncf.f 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵𝑥 ) )
Assertion fprodsub2cncf ( 𝜑𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fprodsub2cncf.k 𝑘 𝜑
2 fprodsub2cncf.a ( 𝜑𝐴 ∈ Fin )
3 fprodsub2cncf.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
4 fprodsub2cncf.f 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵𝑥 ) )
5 4 a1i ( 𝜑𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵𝑥 ) ) )
6 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7 6 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
8 7 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
9 eqid ( 𝑥 ∈ ℂ ↦ ( 𝐵𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐵𝑥 ) )
10 3 9 sub2cncfd ( ( 𝜑𝑘𝐴 ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
11 6 cncfcn1 ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
12 11 a1i ( ( 𝜑𝑘𝐴 ) → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
13 10 12 eleqtrd ( ( 𝜑𝑘𝐴 ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
14 1 6 8 2 13 fprodcn ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
15 5 14 eqeltrd ( 𝜑𝐹 ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
16 11 a1i ( 𝜑 → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17 16 eqcomd ( 𝜑 → ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) = ( ℂ –cn→ ℂ ) )
18 15 17 eleqtrd ( 𝜑𝐹 ∈ ( ℂ –cn→ ℂ ) )