Metamath Proof Explorer

Theorem fprodsub2cncf

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

Ref Expression
Hypotheses fprodsub2cncf.k ⊢ Ⅎ k φ
fprodsub2cncf.a ⊢ φ → A ∈ Fin
fprodsub2cncf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodsub2cncf.f ⊢ F = x ∈ ℂ ⟼ ∏ k ∈ A B − x
Assertion fprodsub2cncf ⊢ φ → F : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 fprodsub2cncf.k ⊢ Ⅎ k φ
2 fprodsub2cncf.a ⊢ φ → A ∈ Fin
3 fprodsub2cncf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 fprodsub2cncf.f ⊢ F = x ∈ ℂ ⟼ ∏ k ∈ A B − x
5 4 a1i ⊢ φ → F = x ∈ ℂ ⟼ ∏ k ∈ A B − x
6 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
7 6 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
8 7 a1i ⊢ φ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
9 eqid ⊢ x ∈ ℂ ⟼ B − x = x ∈ ℂ ⟼ B − x
10 3 9 sub2cncfd ⊢ φ ∧ k ∈ A → x ∈ ℂ ⟼ B − x : ℂ ⟶cn ℂ
11 6 cncfcn1 ⊢ ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
12 11 a1i ⊢ φ ∧ k ∈ A → ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
13 10 12 eleqtrd ⊢ φ ∧ k ∈ A → x ∈ ℂ ⟼ B − x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
14 1 6 8 2 13 fprodcn ⊢ φ → x ∈ ℂ ⟼ ∏ k ∈ A B − x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
15 5 14 eqeltrd ⊢ φ → F ∈ 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 ⊢ φ → F : ℂ ⟶cn ℂ