This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulcncf

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
5 cncfrss 
 |-  ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> X C_ CC )
6 1 5 syl 
 |-  ( ph -> X C_ CC )
7 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ X C_ CC ) -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
8 4 6 7 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
9 ssid 
 |-  CC C_ CC
10 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
11 4 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
12 3 10 11 cncfcn 
 |-  ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
13 6 9 12 sylancl 
 |-  ( ph -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
14 1 13 eleqtrd 
 |-  ( ph -> ( x e. X |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
15 2 13 eleqtrd 
 |-  ( ph -> ( x e. X |-> B ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
16 4 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
17 3 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
18 17 a1i 
 |-  ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
19 oveq12 
 |-  ( ( u = A /\ v = B ) -> ( u x. v ) = ( A x. B ) )
20 8 14 15 16 16 18 19 cnmpt12 
 |-  ( ph -> ( x e. X |-> ( A x. B ) ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
21 20 13 eleqtrrd 
 |-  ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) )