Metamath Proof Explorer

Theorem mulcncff

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mulcncff.f 
|- ( ph -> F e. ( X -cn-> CC ) )
mulcncff.g 
|- ( ph -> G e. ( X -cn-> CC ) )
Assertion mulcncff 
|- ( ph -> ( F oF x. G ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 mulcncff.f 
 |-  ( ph -> F e. ( X -cn-> CC ) )
2 mulcncff.g 
 |-  ( ph -> G e. ( X -cn-> CC ) )
3 cncfrss 
 |-  ( F e. ( X -cn-> CC ) -> X C_ CC )
4 cnex 
 |-  CC e. _V
5 4 ssex 
 |-  ( X C_ CC -> X e. _V )
6 1 3 5 3syl 
 |-  ( ph -> X e. _V )
7 cncff 
 |-  ( F e. ( X -cn-> CC ) -> F : X --> CC )
8 1 7 syl 
 |-  ( ph -> F : X --> CC )
9 8 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
10 cncff 
 |-  ( G e. ( X -cn-> CC ) -> G : X --> CC )
11 2 10 syl 
 |-  ( ph -> G : X --> CC )
12 11 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
13 8 feqmptd 
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
14 11 feqmptd 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
15 6 9 12 13 14 offval2 
 |-  ( ph -> ( F oF x. G ) = ( x e. X |-> ( ( F ` x ) x. ( G ` x ) ) ) )
16 13 1 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( F ` x ) ) e. ( X -cn-> CC ) )
17 14 2 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( G ` x ) ) e. ( X -cn-> CC ) )
18 16 17 mulcncf 
 |-  ( ph -> ( x e. X |-> ( ( F ` x ) x. ( G ` x ) ) ) e. ( X -cn-> CC ) )
19 15 18 eqeltrd 
 |-  ( ph -> ( F oF x. G ) e. ( X -cn-> CC ) )