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