Metamath Proof Explorer

Theorem rmulccn

Description: Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses rmulccn.1 
|- J = ( topGen ` ran (,) )
rmulccn.2 
|- ( ph -> C e. RR )
Assertion rmulccn 
|- ( ph -> ( x e. RR |-> ( x x. C ) ) e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 rmulccn.1 
 |-  J = ( topGen ` ran (,) )
2 rmulccn.2 
 |-  ( ph -> C e. RR )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 3 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
5 4 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
6 5 cnmptid 
 |-  ( ph -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
7 2 recnd 
 |-  ( ph -> C e. CC )
8 5 5 7 cnmptc 
 |-  ( ph -> ( x e. CC |-> C ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
9 3 mpomulcn 
 |-  ( y e. CC , z e. CC |-> ( y x. z ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
10 9 a1i 
 |-  ( ph -> ( y e. CC , z e. CC |-> ( y x. z ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
11 oveq12 
 |-  ( ( y = x /\ z = C ) -> ( y x. z ) = ( x x. C ) )
12 5 6 8 5 5 10 11 cnmpt12 
 |-  ( ph -> ( x e. CC |-> ( x x. C ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
13 ax-resscn 
 |-  RR C_ CC
14 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
15 14 cnrest 
 |-  ( ( ( x e. CC |-> ( x x. C ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ RR C_ CC ) -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) )
16 12 13 15 sylancl 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) )
17 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
18 7 adantr 
 |-  ( ( ph /\ x e. CC ) -> C e. CC )
19 17 18 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( x x. C ) e. CC )
20 19 ralrimiva 
 |-  ( ph -> A. x e. CC ( x x. C ) e. CC )
21 eqid 
 |-  ( x e. CC |-> ( x x. C ) ) = ( x e. CC |-> ( x x. C ) )
22 21 fnmpt 
 |-  ( A. x e. CC ( x x. C ) e. CC -> ( x e. CC |-> ( x x. C ) ) Fn CC )
23 20 22 syl 
 |-  ( ph -> ( x e. CC |-> ( x x. C ) ) Fn CC )
24 13 a1i 
 |-  ( ph -> RR C_ CC )
25 23 24 fnssresd 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) Fn RR )
26 simpr 
 |-  ( ( ph /\ w e. RR ) -> w e. RR )
27 oveq1 
 |-  ( x = w -> ( x x. C ) = ( w x. C ) )
28 resmpt 
 |-  ( RR C_ CC -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) = ( x e. RR |-> ( x x. C ) ) )
29 13 28 ax-mp 
 |-  ( ( x e. CC |-> ( x x. C ) ) |` RR ) = ( x e. RR |-> ( x x. C ) )
30 ovex 
 |-  ( w x. C ) e. _V
31 27 29 30 fvmpt 
 |-  ( w e. RR -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) = ( w x. C ) )
32 26 31 syl 
 |-  ( ( ph /\ w e. RR ) -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) = ( w x. C ) )
33 2 adantr 
 |-  ( ( ph /\ w e. RR ) -> C e. RR )
34 26 33 remulcld 
 |-  ( ( ph /\ w e. RR ) -> ( w x. C ) e. RR )
35 32 34 eqeltrd 
 |-  ( ( ph /\ w e. RR ) -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) e. RR )
36 35 ralrimiva 
 |-  ( ph -> A. w e. RR ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) e. RR )
37 fnfvrnss 
 |-  ( ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) Fn RR /\ A. w e. RR ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) e. RR ) -> ran ( ( x e. CC |-> ( x x. C ) ) |` RR ) C_ RR )
38 25 36 37 syl2anc 
 |-  ( ph -> ran ( ( x e. CC |-> ( x x. C ) ) |` RR ) C_ RR )
39 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( ( x e. CC |-> ( x x. C ) ) |` RR ) C_ RR /\ RR C_ CC ) -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) <-> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
40 4 38 24 39 mp3an2i 
 |-  ( ph -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) <-> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
41 16 40 mpbid 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
42 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
43 1 42 eqtri 
 |-  J = ( ( TopOpen ` CCfld ) |`t RR )
44 43 43 oveq12i 
 |-  ( J Cn J ) = ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) )
45 44 eqcomi 
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) = ( J Cn J )
46 41 29 45 3eltr3g 
 |-  ( ph -> ( x e. RR |-> ( x x. C ) ) e. ( J Cn J ) )