Metamath Proof Explorer

Theorem rmulccn

Description: Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

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 ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
10 ffn ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
11 9 10 ax-mp ⊢ · Fn ( ℂ × ℂ )
12 fnov ⊢ ( · Fn ( ℂ × ℂ ) ↔ · = ( 𝑦 ∈ ℂ , 𝑧 ∈ ℂ ↦ ( 𝑦 · 𝑧 ) ) )
13 11 12 mpbi ⊢ · = ( 𝑦 ∈ ℂ , 𝑧 ∈ ℂ ↦ ( 𝑦 · 𝑧 ) )
14 3 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
15 13 14 eqeltrri ⊢ ( 𝑦 ∈ ℂ , 𝑧 ∈ ℂ ↦ ( 𝑦 · 𝑧 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
16 15 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ , 𝑧 ∈ ℂ ↦ ( 𝑦 · 𝑧 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
17 oveq12 ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = 𝐶 ) → ( 𝑦 · 𝑧 ) = ( 𝑥 · 𝐶 ) )
18 5 6 8 5 5 16 17 cnmpt12 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
19 ax-resscn ⊢ ℝ ⊆ ℂ
20 4 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
21 20 cnrest ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ℝ ⊆ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) )
22 18 19 21 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
24 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐶 ∈ ℂ )
25 23 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · 𝐶 ) ∈ ℂ )
26 25 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( 𝑥 · 𝐶 ) ∈ ℂ )
27 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) )
28 27 fnmpt ⊢ ( ∀ 𝑥 ∈ ℂ ( 𝑥 · 𝐶 ) ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) Fn ℂ )
29 26 28 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) Fn ℂ )
30 fnssres ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) Fn ℂ ∧ ℝ ⊆ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) Fn ℝ )
31 29 19 30 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) Fn ℝ )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
33 fvres ⊢ ( 𝑤 ∈ ℝ → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ‘ 𝑤 ) )
34 recn ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
35 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 · 𝐶 ) = ( 𝑤 · 𝐶 ) )
36 ovex ⊢ ( 𝑤 · 𝐶 ) ∈ V
37 35 27 36 fvmpt ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ‘ 𝑤 ) = ( 𝑤 · 𝐶 ) )
38 34 37 syl ⊢ ( 𝑤 ∈ ℝ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ‘ 𝑤 ) = ( 𝑤 · 𝐶 ) )
39 33 38 eqtrd ⊢ ( 𝑤 ∈ ℝ → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) = ( 𝑤 · 𝐶 ) )
40 32 39 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) = ( 𝑤 · 𝐶 ) )
41 2 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐶 ∈ ℝ )
42 32 41 remulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝑤 · 𝐶 ) ∈ ℝ )
43 40 42 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) ∈ ℝ )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) ∈ ℝ )
45 fnfvrnss ⊢ ( ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) Fn ℝ ∧ ∀ 𝑤 ∈ ℝ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ‘ 𝑤 ) ∈ ℝ ) → ran ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ⊆ ℝ )
46 31 44 45 syl2anc ⊢ ( 𝜑 → ran ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ⊆ ℝ )
47 19 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
48 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
49 5 46 47 48 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
50 22 49 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
51 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) )
52 19 51 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 · 𝐶 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) )
53 3 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
54 1 53 eqtri ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
55 54 54 oveq12i ⊢ ( 𝐽 Cn 𝐽 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
56 55 eqcomi ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) = ( 𝐽 Cn 𝐽 )
57 50 52 56 3eltr3g ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝑥 · 𝐶 ) ) ∈ ( 𝐽 Cn 𝐽 ) )