Metamath Proof Explorer

Theorem xrmulc1cn

Description: The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Hypotheses xrmulc1cn.k 
|- J = ( ordTop ` <_ )
xrmulc1cn.f 
|- F = ( x e. RR* |-> ( x *e C ) )
xrmulc1cn.c 
|- ( ph -> C e. RR+ )
Assertion xrmulc1cn 
|- ( ph -> F e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 xrmulc1cn.k 
 |-  J = ( ordTop ` <_ )
2 xrmulc1cn.f 
 |-  F = ( x e. RR* |-> ( x *e C ) )
3 xrmulc1cn.c 
 |-  ( ph -> C e. RR+ )
4 letsr 
 |-  <_ e. TosetRel
5 4 a1i 
 |-  ( ph -> <_ e. TosetRel )
6 simpr 
 |-  ( ( ph /\ x e. RR* ) -> x e. RR* )
7 3 adantr 
 |-  ( ( ph /\ x e. RR* ) -> C e. RR+ )
8 7 rpxrd 
 |-  ( ( ph /\ x e. RR* ) -> C e. RR* )
9 6 8 xmulcld 
 |-  ( ( ph /\ x e. RR* ) -> ( x *e C ) e. RR* )
10 9 ralrimiva 
 |-  ( ph -> A. x e. RR* ( x *e C ) e. RR* )
11 simpr 
 |-  ( ( ph /\ y e. RR* ) -> y e. RR* )
12 3 adantr 
 |-  ( ( ph /\ y e. RR* ) -> C e. RR+ )
13 12 rpred 
 |-  ( ( ph /\ y e. RR* ) -> C e. RR )
14 12 rpne0d 
 |-  ( ( ph /\ y e. RR* ) -> C =/= 0 )
15 xreceu 
 |-  ( ( y e. RR* /\ C e. RR /\ C =/= 0 ) -> E! x e. RR* ( C *e x ) = y )
16 11 13 14 15 syl3anc 
 |-  ( ( ph /\ y e. RR* ) -> E! x e. RR* ( C *e x ) = y )
17 eqcom 
 |-  ( y = ( x *e C ) <-> ( x *e C ) = y )
18 simpr 
 |-  ( ( ( ph /\ y e. RR* ) /\ x e. RR* ) -> x e. RR* )
19 8 adantlr 
 |-  ( ( ( ph /\ y e. RR* ) /\ x e. RR* ) -> C e. RR* )
20 xmulcom 
 |-  ( ( x e. RR* /\ C e. RR* ) -> ( x *e C ) = ( C *e x ) )
21 18 19 20 syl2anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ x e. RR* ) -> ( x *e C ) = ( C *e x ) )
22 21 eqeq1d 
 |-  ( ( ( ph /\ y e. RR* ) /\ x e. RR* ) -> ( ( x *e C ) = y <-> ( C *e x ) = y ) )
23 17 22 bitrid 
 |-  ( ( ( ph /\ y e. RR* ) /\ x e. RR* ) -> ( y = ( x *e C ) <-> ( C *e x ) = y ) )
24 23 reubidva 
 |-  ( ( ph /\ y e. RR* ) -> ( E! x e. RR* y = ( x *e C ) <-> E! x e. RR* ( C *e x ) = y ) )
25 16 24 mpbird 
 |-  ( ( ph /\ y e. RR* ) -> E! x e. RR* y = ( x *e C ) )
26 25 ralrimiva 
 |-  ( ph -> A. y e. RR* E! x e. RR* y = ( x *e C ) )
27 2 f1ompt 
 |-  ( F : RR* -1-1-onto-> RR* <-> ( A. x e. RR* ( x *e C ) e. RR* /\ A. y e. RR* E! x e. RR* y = ( x *e C ) ) )
28 10 26 27 sylanbrc 
 |-  ( ph -> F : RR* -1-1-onto-> RR* )
29 simplr 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> x e. RR* )
30 simpr 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> y e. RR* )
31 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> C e. RR+ )
32 xlemul1 
 |-  ( ( x e. RR* /\ y e. RR* /\ C e. RR+ ) -> ( x <_ y <-> ( x *e C ) <_ ( y *e C ) ) )
33 29 30 31 32 syl3anc 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> ( x <_ y <-> ( x *e C ) <_ ( y *e C ) ) )
34 ovex 
 |-  ( x *e C ) e. _V
35 2 fvmpt2 
 |-  ( ( x e. RR* /\ ( x *e C ) e. _V ) -> ( F ` x ) = ( x *e C ) )
36 29 34 35 sylancl 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> ( F ` x ) = ( x *e C ) )
37 oveq1 
 |-  ( x = y -> ( x *e C ) = ( y *e C ) )
38 ovex 
 |-  ( y *e C ) e. _V
39 37 2 38 fvmpt 
 |-  ( y e. RR* -> ( F ` y ) = ( y *e C ) )
40 39 adantl 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> ( F ` y ) = ( y *e C ) )
41 36 40 breq12d 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> ( ( F ` x ) <_ ( F ` y ) <-> ( x *e C ) <_ ( y *e C ) ) )
42 33 41 bitr4d 
 |-  ( ( ( ph /\ x e. RR* ) /\ y e. RR* ) -> ( x <_ y <-> ( F ` x ) <_ ( F ` y ) ) )
43 42 ralrimiva 
 |-  ( ( ph /\ x e. RR* ) -> A. y e. RR* ( x <_ y <-> ( F ` x ) <_ ( F ` y ) ) )
44 43 ralrimiva 
 |-  ( ph -> A. x e. RR* A. y e. RR* ( x <_ y <-> ( F ` x ) <_ ( F ` y ) ) )
45 df-isom 
 |-  ( F Isom <_ , <_ ( RR* , RR* ) <-> ( F : RR* -1-1-onto-> RR* /\ A. x e. RR* A. y e. RR* ( x <_ y <-> ( F ` x ) <_ ( F ` y ) ) ) )
46 28 44 45 sylanbrc 
 |-  ( ph -> F Isom <_ , <_ ( RR* , RR* ) )
47 ledm 
 |-  RR* = dom <_
48 47 47 ordthmeolem 
 |-  ( ( <_ e. TosetRel /\ <_ e. TosetRel /\ F Isom <_ , <_ ( RR* , RR* ) ) -> F e. ( ( ordTop ` <_ ) Cn ( ordTop ` <_ ) ) )
49 5 5 46 48 syl3anc 
 |-  ( ph -> F e. ( ( ordTop ` <_ ) Cn ( ordTop ` <_ ) ) )
50 1 1 oveq12i 
 |-  ( J Cn J ) = ( ( ordTop ` <_ ) Cn ( ordTop ` <_ ) )
51 49 50 eleqtrrdi 
 |-  ( ph -> F e. ( J Cn J ) )