Metamath Proof Explorer


Theorem fprodadd2cncf

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

Ref Expression
Hypotheses fprodadd2cncf.k k φ
fprodadd2cncf.a φ A Fin
fprodadd2cncf.b φ k A B
fprodadd2cncf.f F = x k A B + x
Assertion fprodadd2cncf φ F : cn

Proof

Step Hyp Ref Expression
1 fprodadd2cncf.k k φ
2 fprodadd2cncf.a φ A Fin
3 fprodadd2cncf.b φ k A B
4 fprodadd2cncf.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 add2cncf φ 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