Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0mulc1cn Structured version   Visualization version   GIF version

Theorem xrge0mulc1cn 30217
Description: The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
Hypotheses
Ref Expression
xrge0mulc1cn.k 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
xrge0mulc1cn.f 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
xrge0mulc1cn.c (𝜑𝐶 ∈ (0[,)+∞))
Assertion
Ref Expression
xrge0mulc1cn (𝜑𝐹 ∈ (𝐽 Cn 𝐽))
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐹(𝑥)   𝐽(𝑥)

Proof of Theorem xrge0mulc1cn
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 xrge0mulc1cn.k . . . . . 6 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
2 letopon 21132 . . . . . . 7 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
3 iccssxr 12370 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
4 resttopon 21088 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ (0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞)))
52, 3, 4mp2an 710 . . . . . 6 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞))
61, 5eqeltri 2799 . . . . 5 𝐽 ∈ (TopOn‘(0[,]+∞))
76a1i 11 . . . 4 (𝐶 = 0 → 𝐽 ∈ (TopOn‘(0[,]+∞)))
8 0e0iccpnf 12397 . . . . 5 0 ∈ (0[,]+∞)
98a1i 11 . . . 4 (𝐶 = 0 → 0 ∈ (0[,]+∞))
10 simpl 474 . . . . . . . . 9 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝐶 = 0)
1110oveq2d 6781 . . . . . . . 8 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = (𝑥 ·e 0))
12 simpr 479 . . . . . . . . . 10 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ (0[,]+∞))
133, 12sseldi 3707 . . . . . . . . 9 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ ℝ*)
14 xmul01 12211 . . . . . . . . 9 (𝑥 ∈ ℝ* → (𝑥 ·e 0) = 0)
1513, 14syl 17 . . . . . . . 8 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 0) = 0)
1611, 15eqtrd 2758 . . . . . . 7 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = 0)
1716mpteq2dva 4852 . . . . . 6 (𝐶 = 0 → (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) = (𝑥 ∈ (0[,]+∞) ↦ 0))
18 xrge0mulc1cn.f . . . . . 6 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
19 fconstmpt 5272 . . . . . 6 ((0[,]+∞) × {0}) = (𝑥 ∈ (0[,]+∞) ↦ 0)
2017, 18, 193eqtr4g 2783 . . . . 5 (𝐶 = 0 → 𝐹 = ((0[,]+∞) × {0}))
21 c0ex 10147 . . . . . 6 0 ∈ V
2221fconst2 6586 . . . . 5 (𝐹:(0[,]+∞)⟶{0} ↔ 𝐹 = ((0[,]+∞) × {0}))
2320, 22sylibr 224 . . . 4 (𝐶 = 0 → 𝐹:(0[,]+∞)⟶{0})
24 cnconst 21211 . . . 4 (((𝐽 ∈ (TopOn‘(0[,]+∞)) ∧ 𝐽 ∈ (TopOn‘(0[,]+∞))) ∧ (0 ∈ (0[,]+∞) ∧ 𝐹:(0[,]+∞)⟶{0})) → 𝐹 ∈ (𝐽 Cn 𝐽))
257, 7, 9, 23, 24syl22anc 1440 . . 3 (𝐶 = 0 → 𝐹 ∈ (𝐽 Cn 𝐽))
2625adantl 473 . 2 ((𝜑𝐶 = 0) → 𝐹 ∈ (𝐽 Cn 𝐽))
27 eqid 2724 . . . . . . . . 9 (ordTop‘ ≤ ) = (ordTop‘ ≤ )
28 oveq1 6772 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶))
2928cbvmptv 4858 . . . . . . . . 9 (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) = (𝑦 ∈ ℝ* ↦ (𝑦 ·e 𝐶))
30 id 22 . . . . . . . . 9 (𝐶 ∈ ℝ+𝐶 ∈ ℝ+)
3127, 29, 30xrmulc1cn 30206 . . . . . . . 8 (𝐶 ∈ ℝ+ → (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )))
32 letopuni 21134 . . . . . . . . 9 * = (ordTop‘ ≤ )
3332cnrest 21212 . . . . . . . 8 (((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )) ∧ (0[,]+∞) ⊆ ℝ*) → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )))
3431, 3, 33sylancl 697 . . . . . . 7 (𝐶 ∈ ℝ+ → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )))
35 resmpt 5559 . . . . . . . . 9 ((0[,]+∞) ⊆ ℝ* → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)))
363, 35ax-mp 5 . . . . . . . 8 ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
3736, 18eqtr4i 2749 . . . . . . 7 ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = 𝐹
381eqcomi 2733 . . . . . . . 8 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = 𝐽
3938oveq1i 6775 . . . . . . 7 (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )) = (𝐽 Cn (ordTop‘ ≤ ))
4034, 37, 393eltr3g 2819 . . . . . 6 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )))
412a1i 11 . . . . . . 7 (𝐶 ∈ ℝ+ → (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*))
42 simpr 479 . . . . . . . . . 10 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ (0[,]+∞))
43 ioorp 12365 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
44 ioossicc 12373 . . . . . . . . . . . 12 (0(,)+∞) ⊆ (0[,]+∞)
4543, 44eqsstr3i 3742 . . . . . . . . . . 11 + ⊆ (0[,]+∞)
46 simpl 474 . . . . . . . . . . 11 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝐶 ∈ ℝ+)
4745, 46sseldi 3707 . . . . . . . . . 10 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝐶 ∈ (0[,]+∞))
48 ge0xmulcl 12401 . . . . . . . . . 10 ((𝑥 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) ∈ (0[,]+∞))
4942, 47, 48syl2anc 696 . . . . . . . . 9 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) ∈ (0[,]+∞))
5049, 18fmptd 6500 . . . . . . . 8 (𝐶 ∈ ℝ+𝐹:(0[,]+∞)⟶(0[,]+∞))
51 frn 6166 . . . . . . . 8 (𝐹:(0[,]+∞)⟶(0[,]+∞) → ran 𝐹 ⊆ (0[,]+∞))
5250, 51syl 17 . . . . . . 7 (𝐶 ∈ ℝ+ → ran 𝐹 ⊆ (0[,]+∞))
533a1i 11 . . . . . . 7 (𝐶 ∈ ℝ+ → (0[,]+∞) ⊆ ℝ*)
54 cnrest2 21213 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ ran 𝐹 ⊆ (0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))))
5541, 52, 53, 54syl3anc 1439 . . . . . 6 (𝐶 ∈ ℝ+ → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))))
5640, 55mpbid 222 . . . . 5 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞))))
571oveq2i 6776 . . . . 5 (𝐽 Cn 𝐽) = (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))
5856, 57syl6eleqr 2814 . . . 4 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn 𝐽))
5958, 43eleq2s 2821 . . 3 (𝐶 ∈ (0(,)+∞) → 𝐹 ∈ (𝐽 Cn 𝐽))
6059adantl 473 . 2 ((𝜑𝐶 ∈ (0(,)+∞)) → 𝐹 ∈ (𝐽 Cn 𝐽))
61 xrge0mulc1cn.c . . 3 (𝜑𝐶 ∈ (0[,)+∞))
62 0xr 10199 . . . 4 0 ∈ ℝ*
63 pnfxr 10205 . . . 4 +∞ ∈ ℝ*
64 0ltpnf 12070 . . . 4 0 < +∞
65 elicoelioo 29770 . . . 4 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → (𝐶 ∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞))))
6662, 63, 64, 65mp3an 1537 . . 3 (𝐶 ∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))
6761, 66sylib 208 . 2 (𝜑 → (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))
6826, 60, 67mpjaodan 862 1 (𝜑𝐹 ∈ (𝐽 Cn 𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1596  wcel 2103  wss 3680  {csn 4285   class class class wbr 4760  cmpt 4837   × cxp 5216  ran crn 5219  cres 5220  wf 5997  cfv 6001  (class class class)co 6765  0cc0 10049  +∞cpnf 10184  *cxr 10186   < clt 10187  cle 10188  +crp 11946   ·e cxmu 12059  (,)cioo 12289  [,)cico 12291  [,]cicc 12292  t crest 16204  ordTopcordt 16282  TopOnctopon 20838   Cn ccn 21151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-fi 8433  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-rp 11947  df-xneg 12060  df-xmul 12062  df-ioo 12293  df-ico 12295  df-icc 12296  df-rest 16206  df-topgen 16227  df-ordt 16284  df-ps 17322  df-tsr 17323  df-top 20822  df-topon 20839  df-bases 20873  df-cn 21154  df-cnp 21155
This theorem is referenced by:  esummulc1  30373
  Copyright terms: Public domain W3C validator