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 ∈ ℝ * ⟼ x ⋅ 𝑒 C
xrmulc1cn.c ⊢ φ → C ∈ ℝ +
Assertion xrmulc1cn ⊢ φ → F ∈ J Cn J

Proof

Step Hyp Ref Expression
1 xrmulc1cn.k ⊢ J = ordTop ⁡ ≤
2 xrmulc1cn.f ⊢ F = x ∈ ℝ * ⟼ x ⋅ 𝑒 C
3 xrmulc1cn.c ⊢ φ → C ∈ ℝ +
4 letsr ⊢ ≤ ∈ TosetRel
5 4 a1i ⊢ φ → ≤ ∈ TosetRel
6 simpr ⊢ φ ∧ x ∈ ℝ * → x ∈ ℝ *
7 3 adantr ⊢ φ ∧ x ∈ ℝ * → C ∈ ℝ +
8 7 rpxrd ⊢ φ ∧ x ∈ ℝ * → C ∈ ℝ *
9 6 8 xmulcld ⊢ φ ∧ x ∈ ℝ * → x ⋅ 𝑒 C ∈ ℝ *
10 9 ralrimiva ⊢ φ → ∀ x ∈ ℝ * x ⋅ 𝑒 C ∈ ℝ *
11 simpr ⊢ φ ∧ y ∈ ℝ * → y ∈ ℝ *
12 3 adantr ⊢ φ ∧ y ∈ ℝ * → C ∈ ℝ +
13 12 rpred ⊢ φ ∧ y ∈ ℝ * → C ∈ ℝ
14 12 rpne0d ⊢ φ ∧ y ∈ ℝ * → C ≠ 0
15 xreceu ⊢ y ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → ∃! x ∈ ℝ * C ⋅ 𝑒 x = y
16 11 13 14 15 syl3anc ⊢ φ ∧ y ∈ ℝ * → ∃! x ∈ ℝ * C ⋅ 𝑒 x = y
17 eqcom ⊢ y = x ⋅ 𝑒 C ↔ x ⋅ 𝑒 C = y
18 simpr ⊢ φ ∧ y ∈ ℝ * ∧ x ∈ ℝ * → x ∈ ℝ *
19 8 adantlr ⊢ φ ∧ y ∈ ℝ * ∧ x ∈ ℝ * → C ∈ ℝ *
20 xmulcom ⊢ x ∈ ℝ * ∧ C ∈ ℝ * → x ⋅ 𝑒 C = C ⋅ 𝑒 x
21 18 19 20 syl2anc ⊢ φ ∧ y ∈ ℝ * ∧ x ∈ ℝ * → x ⋅ 𝑒 C = C ⋅ 𝑒 x
22 21 eqeq1d ⊢ φ ∧ y ∈ ℝ * ∧ x ∈ ℝ * → x ⋅ 𝑒 C = y ↔ C ⋅ 𝑒 x = y
23 17 22 bitrid ⊢ φ ∧ y ∈ ℝ * ∧ x ∈ ℝ * → y = x ⋅ 𝑒 C ↔ C ⋅ 𝑒 x = y
24 23 reubidva ⊢ φ ∧ y ∈ ℝ * → ∃! x ∈ ℝ * y = x ⋅ 𝑒 C ↔ ∃! x ∈ ℝ * C ⋅ 𝑒 x = y
25 16 24 mpbird ⊢ φ ∧ y ∈ ℝ * → ∃! x ∈ ℝ * y = x ⋅ 𝑒 C
26 25 ralrimiva ⊢ φ → ∀ y ∈ ℝ * ∃! x ∈ ℝ * y = x ⋅ 𝑒 C
27 2 f1ompt ⊢ F : ℝ * ⟶ 1-1 onto ℝ * ↔ ∀ x ∈ ℝ * x ⋅ 𝑒 C ∈ ℝ * ∧ ∀ y ∈ ℝ * ∃! x ∈ ℝ * y = x ⋅ 𝑒 C
28 10 26 27 sylanbrc ⊢ φ → F : ℝ * ⟶ 1-1 onto ℝ *
29 simplr ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → x ∈ ℝ *
30 simpr ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → y ∈ ℝ *
31 3 ad2antrr ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → C ∈ ℝ +
32 xlemul1 ⊢ x ∈ ℝ * ∧ y ∈ ℝ * ∧ C ∈ ℝ + → x ≤ y ↔ x ⋅ 𝑒 C ≤ y ⋅ 𝑒 C
33 29 30 31 32 syl3anc ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → x ≤ y ↔ x ⋅ 𝑒 C ≤ y ⋅ 𝑒 C
34 ovex ⊢ x ⋅ 𝑒 C ∈ V
35 2 fvmpt2 ⊢ x ∈ ℝ * ∧ x ⋅ 𝑒 C ∈ V → F ⁡ x = x ⋅ 𝑒 C
36 29 34 35 sylancl ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → F ⁡ x = x ⋅ 𝑒 C
37 oveq1 ⊢ x = y → x ⋅ 𝑒 C = y ⋅ 𝑒 C
38 ovex ⊢ y ⋅ 𝑒 C ∈ V
39 37 2 38 fvmpt ⊢ y ∈ ℝ * → F ⁡ y = y ⋅ 𝑒 C
40 39 adantl ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → F ⁡ y = y ⋅ 𝑒 C
41 36 40 breq12d ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → F ⁡ x ≤ F ⁡ y ↔ x ⋅ 𝑒 C ≤ y ⋅ 𝑒 C
42 33 41 bitr4d ⊢ φ ∧ x ∈ ℝ * ∧ y ∈ ℝ * → x ≤ y ↔ F ⁡ x ≤ F ⁡ y
43 42 ralrimiva ⊢ φ ∧ x ∈ ℝ * → ∀ y ∈ ℝ * x ≤ y ↔ F ⁡ x ≤ F ⁡ y
44 43 ralrimiva ⊢ φ → ∀ x ∈ ℝ * ∀ y ∈ ℝ * x ≤ y ↔ F ⁡ x ≤ F ⁡ y
45 df-isom ⊢ F Isom ≤ , ≤ ℝ * ℝ * ↔ F : ℝ * ⟶ 1-1 onto ℝ * ∧ ∀ x ∈ ℝ * ∀ y ∈ ℝ * x ≤ y ↔ F ⁡ x ≤ F ⁡ y
46 28 44 45 sylanbrc ⊢ φ → F Isom ≤ , ≤ ℝ * ℝ *
47 ledm ⊢ ℝ * = dom ⁡ ≤
48 47 47 ordthmeolem ⊢ ≤ ∈ TosetRel ∧ ≤ ∈ TosetRel ∧ F Isom ≤ , ≤ ℝ * ℝ * → F ∈ ordTop ⁡ ≤ Cn ordTop ⁡ ≤
49 5 5 46 48 syl3anc ⊢ φ → F ∈ ordTop ⁡ ≤ Cn ordTop ⁡ ≤
50 1 1 oveq12i ⊢ J Cn J = ordTop ⁡ ≤ Cn ordTop ⁡ ≤
51 49 50 eleqtrrdi ⊢ φ → F ∈ J Cn J