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	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	gg-rmulccn.2	$$⊢\phi \to C\in ℝ$$
Assertion	gg-rmulccn	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\in \left(J\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		gg-rmulccn.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		gg-rmulccn.2	$$⊢\phi \to C\in ℝ$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	3	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
5	4	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
6	5	cnmptid	$$⊢\phi \to \left(x\in ℂ⟼x\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
7	2	recnd	$$⊢\phi \to C\in ℂ$$
8	5 5 7	cnmptc	$$⊢\phi \to \left(x\in ℂ⟼C\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
9	3	mpomulcn	$$⊢\left(y\in ℂ,z\in ℂ⟼yz\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
10	9	a1i	$$⊢\phi \to \left(y\in ℂ,z\in ℂ⟼yz\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
11		oveq12	$$⊢\left(y=x\wedge z=C\right)\to yz=xC$$
12	5 6 8 5 5 10 11	cnmpt12	$$⊢\phi \to \left(x\in ℂ⟼xC\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
13		ax-resscn	$$⊢ℝ\subseteq ℂ$$
14	4	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
15	14	cnrest	$$⊢\left(\left(x\in ℂ⟼xC\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ℝ\subseteq ℂ\right)\to {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
16	12 13 15	sylancl	$$⊢\phi \to {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
17		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
18	7	adantr	$$⊢\left(\phi \wedge x\in ℂ\right)\to C\in ℂ$$
19	17 18	mulcld	$$⊢\left(\phi \wedge x\in ℂ\right)\to xC\in ℂ$$
20	19	ralrimiva	$$⊢\phi \to \forall x\in ℂxC\in ℂ$$
21		eqid	$$⊢\left(x\in ℂ⟼xC\right)=\left(x\in ℂ⟼xC\right)$$
22	21	fnmpt	$$⊢\forall x\in ℂxC\in ℂ\to \left(x\in ℂ⟼xC\right)Fnℂ$$
23	20 22	syl	$$⊢\phi \to \left(x\in ℂ⟼xC\right)Fnℂ$$
24		fnssres	$$⊢\left(\left(x\in ℂ⟼xC\right)Fnℂ\wedge ℝ\subseteq ℂ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)Fnℝ$$
25	23 13 24	sylancl	$$⊢\phi \to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)Fnℝ$$
26		simpr	$$⊢\left(\phi \wedge w\in ℝ\right)\to w\in ℝ$$
27		fvres	$$⊢w\in ℝ\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=\left(x\in ℂ⟼xC\right)\left(w\right)$$
28		recn	$$⊢w\in ℝ\to w\in ℂ$$
29		oveq1	$$⊢x=w\to xC=wC$$
30		ovex	$$⊢wC\in \mathrm{V}$$
31	29 21 30	fvmpt	$$⊢w\in ℂ\to \left(x\in ℂ⟼xC\right)\left(w\right)=wC$$
32	28 31	syl	$$⊢w\in ℝ\to \left(x\in ℂ⟼xC\right)\left(w\right)=wC$$
33	27 32	eqtrd	$$⊢w\in ℝ\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=wC$$
34	26 33	syl	$$⊢\left(\phi \wedge w\in ℝ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=wC$$
35	2	adantr	$$⊢\left(\phi \wedge w\in ℝ\right)\to C\in ℝ$$
36	26 35	remulcld	$$⊢\left(\phi \wedge w\in ℝ\right)\to wC\in ℝ$$
37	34 36	eqeltrd	$$⊢\left(\phi \wedge w\in ℝ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)\in ℝ$$
38	37	ralrimiva	$$⊢\phi \to \forall w\in ℝ\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)\in ℝ$$
39		fnfvrnss	$$⊢\left(\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)Fnℝ\wedge \forall w\in ℝ\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)\in ℝ\right)\to \mathrm{ran}\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\subseteq ℝ$$
40	25 38 39	syl2anc	$$⊢\phi \to \mathrm{ran}\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\subseteq ℝ$$
41	13	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
42		cnrest2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\leftrightarrow {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
43	5 40 41 42	syl3anc	$$⊢\phi \to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\leftrightarrow {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
44	16 43	mpbid	$$⊢\phi \to {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)$$
45		resmpt	$$⊢ℝ\subseteq ℂ\to {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼xC\right)$$
46	13 45	ax-mp	$$⊢{\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼xC\right)$$
47	3	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
48	1 47	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
49	48 48	oveq12i	$$⊢J\mathrm{Cn}J=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)$$
50	49	eqcomi	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)=J\mathrm{Cn}J$$
51	44 46 50	3eltr3g	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\in \left(J\mathrm{Cn}J\right)$$