Metamath Proof Explorer

Theorem xrge0mulc1cn

Description: The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses xrge0mulc1cn.k 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
xrge0mulc1cn.f 
|- F = ( x e. ( 0 [,] +oo ) |-> ( x *e C ) )
xrge0mulc1cn.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
Assertion xrge0mulc1cn 
|- ( ph -> F e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 xrge0mulc1cn.k 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
2 xrge0mulc1cn.f 
 |-  F = ( x e. ( 0 [,] +oo ) |-> ( x *e C ) )
3 xrge0mulc1cn.c 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
4 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) )
7 4 5 6 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) )
8 1 7 eqeltri 
 |-  J e. ( TopOn ` ( 0 [,] +oo ) )
9 8 a1i 
 |-  ( C = 0 -> J e. ( TopOn ` ( 0 [,] +oo ) ) )
10 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
11 10 a1i 
 |-  ( C = 0 -> 0 e. ( 0 [,] +oo ) )
12 simpl 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> C = 0 )
13 12 oveq2d 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> ( x *e C ) = ( x *e 0 ) )
14 simpr 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> x e. ( 0 [,] +oo ) )
15 5 14 sseldi 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> x e. RR* )
16 xmul01 
 |-  ( x e. RR* -> ( x *e 0 ) = 0 )
17 15 16 syl 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> ( x *e 0 ) = 0 )
18 13 17 eqtrd 
 |-  ( ( C = 0 /\ x e. ( 0 [,] +oo ) ) -> ( x *e C ) = 0 )
19 18 mpteq2dva 
 |-  ( C = 0 -> ( x e. ( 0 [,] +oo ) |-> ( x *e C ) ) = ( x e. ( 0 [,] +oo ) |-> 0 ) )
20 fconstmpt 
 |-  ( ( 0 [,] +oo ) X. { 0 } ) = ( x e. ( 0 [,] +oo ) |-> 0 )
21 19 2 20 3eqtr4g 
 |-  ( C = 0 -> F = ( ( 0 [,] +oo ) X. { 0 } ) )
22 c0ex 
 |-  0 e. _V
23 22 fconst2 
 |-  ( F : ( 0 [,] +oo ) --> { 0 } <-> F = ( ( 0 [,] +oo ) X. { 0 } ) )
24 21 23 sylibr 
 |-  ( C = 0 -> F : ( 0 [,] +oo ) --> { 0 } )
25 cnconst 
 |-  ( ( ( J e. ( TopOn ` ( 0 [,] +oo ) ) /\ J e. ( TopOn ` ( 0 [,] +oo ) ) ) /\ ( 0 e. ( 0 [,] +oo ) /\ F : ( 0 [,] +oo ) --> { 0 } ) ) -> F e. ( J Cn J ) )
26 9 9 11 24 25 syl22anc 
 |-  ( C = 0 -> F e. ( J Cn J ) )
27 26 adantl 
 |-  ( ( ph /\ C = 0 ) -> F e. ( J Cn J ) )
28 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
29 oveq1 
 |-  ( x = y -> ( x *e C ) = ( y *e C ) )
30 29 cbvmptv 
 |-  ( x e. RR* |-> ( x *e C ) ) = ( y e. RR* |-> ( y *e C ) )
31 id 
 |-  ( C e. RR+ -> C e. RR+ )
32 28 30 31 xrmulc1cn 
 |-  ( C e. RR+ -> ( x e. RR* |-> ( x *e C ) ) e. ( ( ordTop ` <_ ) Cn ( ordTop ` <_ ) ) )
33 letopuni 
 |-  RR* = U. ( ordTop ` <_ )
34 33 cnrest 
 |-  ( ( ( x e. RR* |-> ( x *e C ) ) e. ( ( ordTop ` <_ ) Cn ( ordTop ` <_ ) ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( x e. RR* |-> ( x *e C ) ) |` ( 0 [,] +oo ) ) e. ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) Cn ( ordTop ` <_ ) ) )
35 32 5 34 sylancl 
 |-  ( C e. RR+ -> ( ( x e. RR* |-> ( x *e C ) ) |` ( 0 [,] +oo ) ) e. ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) Cn ( ordTop ` <_ ) ) )
36 resmpt 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( ( x e. RR* |-> ( x *e C ) ) |` ( 0 [,] +oo ) ) = ( x e. ( 0 [,] +oo ) |-> ( x *e C ) ) )
37 5 36 ax-mp 
 |-  ( ( x e. RR* |-> ( x *e C ) ) |` ( 0 [,] +oo ) ) = ( x e. ( 0 [,] +oo ) |-> ( x *e C ) )
38 37 2 eqtr4i 
 |-  ( ( x e. RR* |-> ( x *e C ) ) |` ( 0 [,] +oo ) ) = F
39 1 eqcomi 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = J
40 39 oveq1i 
 |-  ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) Cn ( ordTop ` <_ ) ) = ( J Cn ( ordTop ` <_ ) )
41 35 38 40 3eltr3g 
 |-  ( C e. RR+ -> F e. ( J Cn ( ordTop ` <_ ) ) )
42 4 a1i 
 |-  ( C e. RR+ -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
43 simpr 
 |-  ( ( C e. RR+ /\ x e. ( 0 [,] +oo ) ) -> x e. ( 0 [,] +oo ) )
44 ioorp 
 |-  ( 0 (,) +oo ) = RR+
45 ioossicc 
 |-  ( 0 (,) +oo ) C_ ( 0 [,] +oo )
46 44 45 eqsstrri 
 |-  RR+ C_ ( 0 [,] +oo )
47 simpl 
 |-  ( ( C e. RR+ /\ x e. ( 0 [,] +oo ) ) -> C e. RR+ )
48 46 47 sseldi 
 |-  ( ( C e. RR+ /\ x e. ( 0 [,] +oo ) ) -> C e. ( 0 [,] +oo ) )
49 ge0xmulcl 
 |-  ( ( x e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( x *e C ) e. ( 0 [,] +oo ) )
50 43 48 49 syl2anc 
 |-  ( ( C e. RR+ /\ x e. ( 0 [,] +oo ) ) -> ( x *e C ) e. ( 0 [,] +oo ) )
51 50 2 fmptd 
 |-  ( C e. RR+ -> F : ( 0 [,] +oo ) --> ( 0 [,] +oo ) )
52 51 frnd 
 |-  ( C e. RR+ -> ran F C_ ( 0 [,] +oo ) )
53 5 a1i 
 |-  ( C e. RR+ -> ( 0 [,] +oo ) C_ RR* )
54 cnrest2 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ran F C_ ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( F e. ( J Cn ( ordTop ` <_ ) ) <-> F e. ( J Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) ) )
55 42 52 53 54 syl3anc 
 |-  ( C e. RR+ -> ( F e. ( J Cn ( ordTop ` <_ ) ) <-> F e. ( J Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) ) )
56 41 55 mpbid 
 |-  ( C e. RR+ -> F e. ( J Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) )
57 1 oveq2i 
 |-  ( J Cn J ) = ( J Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
58 56 57 eleqtrrdi 
 |-  ( C e. RR+ -> F e. ( J Cn J ) )
59 58 44 eleq2s 
 |-  ( C e. ( 0 (,) +oo ) -> F e. ( J Cn J ) )
60 59 adantl 
 |-  ( ( ph /\ C e. ( 0 (,) +oo ) ) -> F e. ( J Cn J ) )
61 0xr 
 |-  0 e. RR*
62 pnfxr 
 |-  +oo e. RR*
63 0ltpnf 
 |-  0 < +oo
64 elicoelioo 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( C e. ( 0 [,) +oo ) <-> ( C = 0 \/ C e. ( 0 (,) +oo ) ) ) )
65 61 62 63 64 mp3an 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C = 0 \/ C e. ( 0 (,) +oo ) ) )
66 3 65 sylib 
 |-  ( ph -> ( C = 0 \/ C e. ( 0 (,) +oo ) ) )
67 27 60 66 mpjaodan 
 |-  ( ph -> F e. ( J Cn J ) )