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

Proof

Step	Hyp	Ref	Expression
1		gg-rmulccn.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		gg-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 𝐽 ) )