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