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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
rmulccn.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion rmulccn ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

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