Metamath Proof Explorer

Theorem rmulccn

Description: Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses rmulccn.1 ⊢ J = topGen ⁡ ran ⁡ .
rmulccn.2 ⊢ φ → C ∈ ℝ
Assertion rmulccn ⊢ φ → x ∈ ℝ ⟼ x ⁢ C ∈ J Cn J

Proof

Step Hyp Ref Expression
1 rmulccn.1 ⊢ J = topGen ⁡ ran ⁡ .
2 rmulccn.2 ⊢ φ → C ∈ ℝ
3 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
4 3 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
5 4 a1i ⊢ φ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
6 5 cnmptid ⊢ φ → x ∈ ℂ ⟼ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
7 2 recnd ⊢ φ → C ∈ ℂ
8 5 5 7 cnmptc ⊢ φ → x ∈ ℂ ⟼ C ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
9 3 mpomulcn ⊢ y ∈ ℂ , z ∈ ℂ ⟼ y ⁢ z ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
10 9 a1i ⊢ φ → y ∈ ℂ , z ∈ ℂ ⟼ y ⁢ z ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
11 oveq12 ⊢ y = x ∧ z = C → y ⁢ z = x ⁢ C
12 5 6 8 5 5 10 11 cnmpt12 ⊢ φ → x ∈ ℂ ⟼ x ⁢ C ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
13 ax-resscn ⊢ ℝ ⊆ ℂ
14 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
15 14 cnrest ⊢ x ∈ ℂ ⟼ x ⁢ C ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld ∧ ℝ ⊆ ℂ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld
16 12 13 15 sylancl ⊢ φ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld
17 simpr ⊢ φ ∧ x ∈ ℂ → x ∈ ℂ
18 7 adantr ⊢ φ ∧ x ∈ ℂ → C ∈ ℂ
19 17 18 mulcld ⊢ φ ∧ x ∈ ℂ → x ⁢ C ∈ ℂ
20 19 ralrimiva ⊢ φ → ∀ x ∈ ℂ x ⁢ C ∈ ℂ
21 eqid ⊢ x ∈ ℂ ⟼ x ⁢ C = x ∈ ℂ ⟼ x ⁢ C
22 21 fnmpt ⊢ ∀ x ∈ ℂ x ⁢ C ∈ ℂ → x ∈ ℂ ⟼ x ⁢ C Fn ℂ
23 20 22 syl ⊢ φ → x ∈ ℂ ⟼ x ⁢ C Fn ℂ
24 13 a1i ⊢ φ → ℝ ⊆ ℂ
25 23 24 fnssresd ⊢ φ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ Fn ℝ
26 simpr ⊢ φ ∧ w ∈ ℝ → w ∈ ℝ
27 oveq1 ⊢ x = w → x ⁢ C = w ⁢ C
28 resmpt ⊢ ℝ ⊆ ℂ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ = x ∈ ℝ ⟼ x ⁢ C
29 13 28 ax-mp ⊢ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ = x ∈ ℝ ⟼ x ⁢ C
30 ovex ⊢ w ⁢ C ∈ V
31 27 29 30 fvmpt ⊢ w ∈ ℝ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⁡ w = w ⁢ C
32 26 31 syl ⊢ φ ∧ w ∈ ℝ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⁡ w = w ⁢ C
33 2 adantr ⊢ φ ∧ w ∈ ℝ → C ∈ ℝ
34 26 33 remulcld ⊢ φ ∧ w ∈ ℝ → w ⁢ C ∈ ℝ
35 32 34 eqeltrd ⊢ φ ∧ w ∈ ℝ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⁡ w ∈ ℝ
36 35 ralrimiva ⊢ φ → ∀ w ∈ ℝ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⁡ w ∈ ℝ
37 fnfvrnss ⊢ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ Fn ℝ ∧ ∀ w ∈ ℝ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⁡ w ∈ ℝ → ran ⁡ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⊆ ℝ
38 25 36 37 syl2anc ⊢ φ → ran ⁡ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⊆ ℝ
39 cnrest2 ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ ran ⁡ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ⊆ ℝ ∧ ℝ ⊆ ℂ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↔ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
40 4 38 24 39 mp3an2i ⊢ φ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↔ x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
41 16 40 mpbid ⊢ φ → x ∈ ℂ ⟼ x ⁢ C ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
42 3 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
43 1 42 eqtri ⊢ J = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
44 43 43 oveq12i ⊢ J Cn J = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
45 44 eqcomi ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = J Cn J
46 41 29 45 3eltr3g ⊢ φ → x ∈ ℝ ⟼ x ⁢ C ∈ J Cn J