Metamath Proof Explorer


Theorem mulcncf

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses mulcncf.1
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
mulcncf.2
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
Assertion mulcncf
|- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 mulcncf.1
 |-  ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
2 mulcncf.2
 |-  ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
3 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 3 mulcn
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
5 4 a1i
 |-  ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
6 3 5 1 2 cncfmpt2f
 |-  ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) )