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

Proof

Step	Hyp	Ref	Expression
1		rmulccn.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		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		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
10		ffn	$$⊢\times :ℂ\times ℂ⟶ℂ\to \times Fn\left(ℂ\times ℂ\right)$$
11	9 10	ax-mp	$$⊢\times Fn\left(ℂ\times ℂ\right)$$
12		fnov	$$⊢\times Fn\left(ℂ\times ℂ\right)\leftrightarrow \times =\left(y\in ℂ,z\in ℂ⟼yz\right)$$
13	11 12	mpbi	$$⊢\times =\left(y\in ℂ,z\in ℂ⟼yz\right)$$
14	3	mulcn	$$⊢\times \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)$$
15	13 14	eqeltrri	$$⊢\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)$$
16	15	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)$$
17		oveq12	$$⊢\left(y=x\wedge z=C\right)\to yz=xC$$
18	5 6 8 5 5 16 17	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)$$
19		ax-resscn	$$⊢ℝ\subseteq ℂ$$
20	4	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
21	20	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)$$
22	18 19 21	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)$$
23		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
24	7	adantr	$$⊢\left(\phi \wedge x\in ℂ\right)\to C\in ℂ$$
25	23 24	mulcld	$$⊢\left(\phi \wedge x\in ℂ\right)\to xC\in ℂ$$
26	25	ralrimiva	$$⊢\phi \to \forall x\in ℂxC\in ℂ$$
27		eqid	$$⊢\left(x\in ℂ⟼xC\right)=\left(x\in ℂ⟼xC\right)$$
28	27	fnmpt	$$⊢\forall x\in ℂxC\in ℂ\to \left(x\in ℂ⟼xC\right)Fnℂ$$
29	26 28	syl	$$⊢\phi \to \left(x\in ℂ⟼xC\right)Fnℂ$$
30		fnssres	$$⊢\left(\left(x\in ℂ⟼xC\right)Fnℂ\wedge ℝ\subseteq ℂ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)Fnℝ$$
31	29 19 30	sylancl	$$⊢\phi \to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)Fnℝ$$
32		simpr	$$⊢\left(\phi \wedge w\in ℝ\right)\to w\in ℝ$$
33		fvres	$$⊢w\in ℝ\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=\left(x\in ℂ⟼xC\right)\left(w\right)$$
34		recn	$$⊢w\in ℝ\to w\in ℂ$$
35		oveq1	$$⊢x=w\to xC=wC$$
36		ovex	$$⊢wC\in \mathrm{V}$$
37	35 27 36	fvmpt	$$⊢w\in ℂ\to \left(x\in ℂ⟼xC\right)\left(w\right)=wC$$
38	34 37	syl	$$⊢w\in ℝ\to \left(x\in ℂ⟼xC\right)\left(w\right)=wC$$
39	33 38	eqtrd	$$⊢w\in ℝ\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=wC$$
40	32 39	syl	$$⊢\left(\phi \wedge w\in ℝ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)=wC$$
41	2	adantr	$$⊢\left(\phi \wedge w\in ℝ\right)\to C\in ℝ$$
42	32 41	remulcld	$$⊢\left(\phi \wedge w\in ℝ\right)\to wC\in ℝ$$
43	40 42	eqeltrd	$$⊢\left(\phi \wedge w\in ℝ\right)\to \left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)\in ℝ$$
44	43	ralrimiva	$$⊢\phi \to \forall w\in ℝ\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\left(w\right)\in ℝ$$
45		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 ℝ$$
46	31 44 45	syl2anc	$$⊢\phi \to \mathrm{ran}\left({\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}\right)\subseteq ℝ$$
47	19	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
48		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)$$
49	5 46 47 48	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)$$
50	22 49	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)$$
51		resmpt	$$⊢ℝ\subseteq ℂ\to {\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼xC\right)$$
52	19 51	ax-mp	$$⊢{\left(x\in ℂ⟼xC\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼xC\right)$$
53	3	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
54	1 53	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
55	54 54	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)$$
56	55	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$$
57	50 52 56	3eltr3g	$$⊢\phi \to \left(x\in ℝ⟼xC\right)\in \left(J\mathrm{Cn}J\right)$$