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 ) )