Metamath Proof Explorer

Theorem rmulccn

Description: Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

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 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
10 ffn 
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
11 9 10 ax-mp 
 |-  x. Fn ( CC X. CC )
12 fnov 
 |-  ( x. Fn ( CC X. CC ) <-> x. = ( y e. CC , z e. CC |-> ( y x. z ) ) )
13 11 12 mpbi 
 |-  x. = ( y e. CC , z e. CC |-> ( y x. z ) )
14 3 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
15 13 14 eqeltrri 
 |-  ( y e. CC , z e. CC |-> ( y x. z ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
16 15 a1i 
 |-  ( ph -> ( y e. CC , z e. CC |-> ( y x. z ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
17 oveq12 
 |-  ( ( y = x /\ z = C ) -> ( y x. z ) = ( x x. C ) )
18 5 6 8 5 5 16 17 cnmpt12 
 |-  ( ph -> ( x e. CC |-> ( x x. C ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
19 ax-resscn 
 |-  RR C_ CC
20 4 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
21 20 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 ) ) )
22 18 19 21 sylancl 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) )
23 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
24 7 adantr 
 |-  ( ( ph /\ x e. CC ) -> C e. CC )
25 23 24 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( x x. C ) e. CC )
26 25 ralrimiva 
 |-  ( ph -> A. x e. CC ( x x. C ) e. CC )
27 eqid 
 |-  ( x e. CC |-> ( x x. C ) ) = ( x e. CC |-> ( x x. C ) )
28 27 fnmpt 
 |-  ( A. x e. CC ( x x. C ) e. CC -> ( x e. CC |-> ( x x. C ) ) Fn CC )
29 26 28 syl 
 |-  ( ph -> ( x e. CC |-> ( x x. C ) ) Fn CC )
30 fnssres 
 |-  ( ( ( x e. CC |-> ( x x. C ) ) Fn CC /\ RR C_ CC ) -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) Fn RR )
31 29 19 30 sylancl 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) Fn RR )
32 simpr 
 |-  ( ( ph /\ w e. RR ) -> w e. RR )
33 fvres 
 |-  ( w e. RR -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) = ( ( x e. CC |-> ( x x. C ) ) ` w ) )
34 recn 
 |-  ( w e. RR -> w e. CC )
35 oveq1 
 |-  ( x = w -> ( x x. C ) = ( w x. C ) )
36 ovex 
 |-  ( w x. C ) e. _V
37 35 27 36 fvmpt 
 |-  ( w e. CC -> ( ( x e. CC |-> ( x x. C ) ) ` w ) = ( w x. C ) )
38 34 37 syl 
 |-  ( w e. RR -> ( ( x e. CC |-> ( x x. C ) ) ` w ) = ( w x. C ) )
39 33 38 eqtrd 
 |-  ( w e. RR -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) = ( w x. C ) )
40 32 39 syl 
 |-  ( ( ph /\ w e. RR ) -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) = ( w x. C ) )
41 2 adantr 
 |-  ( ( ph /\ w e. RR ) -> C e. RR )
42 32 41 remulcld 
 |-  ( ( ph /\ w e. RR ) -> ( w x. C ) e. RR )
43 40 42 eqeltrd 
 |-  ( ( ph /\ w e. RR ) -> ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) e. RR )
44 43 ralrimiva 
 |-  ( ph -> A. w e. RR ( ( ( x e. CC |-> ( x x. C ) ) |` RR ) ` w ) e. RR )
45 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 )
46 31 44 45 syl2anc 
 |-  ( ph -> ran ( ( x e. CC |-> ( x x. C ) ) |` RR ) C_ RR )
47 19 a1i 
 |-  ( ph -> RR C_ CC )
48 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 ) ) ) )
49 5 46 47 48 syl3anc 
 |-  ( 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 ) ) ) )
50 22 49 mpbid 
 |-  ( ph -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
51 resmpt 
 |-  ( RR C_ CC -> ( ( x e. CC |-> ( x x. C ) ) |` RR ) = ( x e. RR |-> ( x x. C ) ) )
52 19 51 ax-mp 
 |-  ( ( x e. CC |-> ( x x. C ) ) |` RR ) = ( x e. RR |-> ( x x. C ) )
53 3 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
54 1 53 eqtri 
 |-  J = ( ( TopOpen ` CCfld ) |`t RR )
55 54 54 oveq12i 
 |-  ( J Cn J ) = ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) )
56 55 eqcomi 
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) = ( J Cn J )
57 50 52 56 3eltr3g 
 |-  ( ph -> ( x e. RR |-> ( x x. C ) ) e. ( J Cn J ) )