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