Theorem dvmptconst

Description: Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvmptconst.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptconst.a	$$⊢\phi \to A\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	dvmptconst.b	$$⊢\phi \to B\in ℂ$$
Assertion	dvmptconst	$$⊢\phi \to \frac{d\left(x\in A⟼B\right)}{d_{S}x}=\left(x\in A⟼0\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptconst.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptconst.a	$$⊢\phi \to A\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		dvmptconst.b	$$⊢\phi \to B\in ℂ$$
4	3	adantr	$$⊢\left(\phi \wedge x\in S\right)\to B\in ℂ$$
5		0red	$$⊢\left(\phi \wedge x\in S\right)\to 0\in ℝ$$
6	1 3	dvmptc	$$⊢\phi \to \frac{d\left(x\in S⟼B\right)}{d_{S}x}=\left(x\in S⟼0\right)$$
7		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
9	8	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
10		ax-resscn	$$⊢ℝ\subseteq ℂ$$
11		sseq1	$$⊢S=ℝ\to \left(S\subseteq ℂ\leftrightarrow ℝ\subseteq ℂ\right)$$
12	10 11	mpbiri	$$⊢S=ℝ\to S\subseteq ℂ$$
13		eqimss	$$⊢S=ℂ\to S\subseteq ℂ$$
14	12 13	pm3.2i	$$⊢\left(\left(S=ℝ\to S\subseteq ℂ\right)\wedge \left(S=ℂ\to S\subseteq ℂ\right)\right)$$
15		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
16	1 15	syl	$$⊢\phi \to \left(S=ℝ\vee S=ℂ\right)$$
17		pm3.44	$$⊢\left(\left(S=ℝ\to S\subseteq ℂ\right)\wedge \left(S=ℂ\to S\subseteq ℂ\right)\right)\to \left(\left(S=ℝ\vee S=ℂ\right)\to S\subseteq ℂ\right)$$
18	14 16 17	mpsyl	$$⊢\phi \to S\subseteq ℂ$$
19		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge S\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
20	9 18 19	syl2anc	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
21		toponss	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)\wedge A\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\right)\to A\subseteq S$$
22	20 2 21	syl2anc	$$⊢\phi \to A\subseteq S$$
23		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S$$
24	1 4 5 6 22 23 7 2	dvmptres	$$⊢\phi \to \frac{d\left(x\in A⟼B\right)}{d_{S}x}=\left(x\in A⟼0\right)$$