Metamath Proof Explorer

Theorem mpomulcn

Description: Complex number multiplication is a continuous function. Version of mulcn using maps-to notation, which does not require ax-mulf . (Contributed by GG, 16-Mar-2025)

Ref Expression
Hypothesis mpomulcn.j 
|- J = ( TopOpen ` CCfld )
Assertion mpomulcn 
|- ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( J tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 mpomulcn.j 
 |-  J = ( TopOpen ` CCfld )
2 mpomulf 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
3 mulcn2 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> E. z e. RR+ E. w e. RR+ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) )
4 simplr 
 |-  ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) -> u e. CC )
5 simplll 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) -> v e. CC )
6 simplr 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> d = u )
7 6 fvoveq1d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( abs ` ( d - b ) ) = ( abs ` ( u - b ) ) )
8 7 breq1d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( abs ` ( d - b ) ) < z <-> ( abs ` ( u - b ) ) < z ) )
9 simpr 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> e = v )
10 9 fvoveq1d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( abs ` ( e - c ) ) = ( abs ` ( v - c ) ) )
11 10 breq1d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( abs ` ( e - c ) ) < w <-> ( abs ` ( v - c ) ) < w ) )
12 8 11 anbi12d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) <-> ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) ) )
13 simplr 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> d = u )
14 13 eqcomd 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> u = d )
15 simpr 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> e = v )
16 15 eqcomd 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> v = e )
17 14 16 oveq12d 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> ( u x. v ) = ( d x. e ) )
18 simplr 
 |-  ( ( ( v e. CC /\ u e. CC ) /\ d = u ) -> u e. CC )
19 simplll 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> v e. CC )
20 tru 
 |-  T.
21 oveq1 
 |-  ( x = u -> ( x x. y ) = ( u x. y ) )
22 oveq2 
 |-  ( y = v -> ( u x. y ) = ( u x. v ) )
23 21 22 cbvmpov 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = ( u e. CC , v e. CC |-> ( u x. v ) )
24 23 a1i 
 |-  ( T. -> ( x e. CC , y e. CC |-> ( x x. y ) ) = ( u e. CC , v e. CC |-> ( u x. v ) ) )
25 eqidd 
 |-  ( T. -> <. u , v >. = <. u , v >. )
26 mulcl 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u x. v ) e. CC )
27 26 3adant1 
 |-  ( ( T. /\ u e. CC /\ v e. CC ) -> ( u x. v ) e. CC )
28 24 25 27 fvmpopr2d 
 |-  ( ( T. /\ u e. CC /\ v e. CC ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( u x. v ) )
29 28 eqcomd 
 |-  ( ( T. /\ u e. CC /\ v e. CC ) -> ( u x. v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) )
30 20 29 mp3an1 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u x. v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) )
31 df-ov 
 |-  ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. )
32 30 31 eqtr4di 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u x. v ) = ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) )
33 18 19 32 syl2an2r 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> ( u x. v ) = ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) )
34 17 33 eqtr3d 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ d = u ) /\ e = v ) -> ( d x. e ) = ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) )
35 34 adantllr 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( d x. e ) = ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) )
36 df-ov 
 |-  ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. b , c >. )
37 oveq1 
 |-  ( x = b -> ( x x. y ) = ( b x. y ) )
38 oveq2 
 |-  ( y = c -> ( b x. y ) = ( b x. c ) )
39 37 38 cbvmpov 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = ( b e. CC , c e. CC |-> ( b x. c ) )
40 39 a1i 
 |-  ( a e. RR+ -> ( x e. CC , y e. CC |-> ( x x. y ) ) = ( b e. CC , c e. CC |-> ( b x. c ) ) )
41 eqidd 
 |-  ( a e. RR+ -> <. b , c >. = <. b , c >. )
42 mulcl 
 |-  ( ( b e. CC /\ c e. CC ) -> ( b x. c ) e. CC )
43 42 3adant1 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( b x. c ) e. CC )
44 40 41 43 fvmpopr2d 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. b , c >. ) = ( b x. c ) )
45 36 44 eqtr2id 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( b x. c ) = ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) )
46 45 ad3antlr 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( b x. c ) = ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) )
47 35 46 oveq12d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( d x. e ) - ( b x. c ) ) = ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) )
48 47 fveq2d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) = ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) )
49 48 breq1d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a <-> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) )
50 12 49 imbi12d 
 |-  ( ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) /\ e = v ) -> ( ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) <-> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
51 5 50 rspcdv 
 |-  ( ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) /\ d = u ) -> ( A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
52 4 51 rspcimdv 
 |-  ( ( ( v e. CC /\ u e. CC ) /\ ( a e. RR+ /\ b e. CC /\ c e. CC ) ) -> ( A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
53 52 expimpd 
 |-  ( ( v e. CC /\ u e. CC ) -> ( ( ( a e. RR+ /\ b e. CC /\ c e. CC ) /\ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) ) -> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
54 53 ex 
 |-  ( v e. CC -> ( u e. CC -> ( ( ( a e. RR+ /\ b e. CC /\ c e. CC ) /\ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) ) -> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) ) )
55 54 com13 
 |-  ( ( ( a e. RR+ /\ b e. CC /\ c e. CC ) /\ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) ) -> ( u e. CC -> ( v e. CC -> ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) ) )
56 55 ralrimdv 
 |-  ( ( ( a e. RR+ /\ b e. CC /\ c e. CC ) /\ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) ) -> ( u e. CC -> A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
57 56 ex 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> ( u e. CC -> A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) ) )
58 57 ralrimdv 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
59 58 reximdv 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( E. w e. RR+ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
60 59 reximdv 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> ( E. z e. RR+ E. w e. RR+ A. d e. CC A. e e. CC ( ( ( abs ` ( d - b ) ) < z /\ ( abs ` ( e - c ) ) < w ) -> ( abs ` ( ( d x. e ) - ( b x. c ) ) ) < a ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) ) )
61 3 60 mpd 
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < z /\ ( abs ` ( v - c ) ) < w ) -> ( abs ` ( ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) - ( b ( x e. CC , y e. CC |-> ( x x. y ) ) c ) ) ) < a ) )
62 1 2 61 addcnlem 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( J tX J ) Cn J )