This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodadd2cncf

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

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

Proof

Step Hyp Ref Expression
1 fprodadd2cncf.k ⊢ Ⅎ 𝑘 𝜑
2 fprodadd2cncf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fprodadd2cncf.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 fprodadd2cncf.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 add2cncf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵 + 𝑥 ) ) ∈ ( ℂ –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→ ℂ ) )