Theorem dvmptc

Description: Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptid.1	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptc.2	$$⊢\phi \to A\in ℂ$$
Assertion	dvmptc	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{S}x}=\left(x\in S⟼0\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptid.1	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptc.2	$$⊢\phi \to A\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		toponmax	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6	4 5	mp1i	$$⊢\phi \to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
8	1 7	syl	$$⊢\phi \to S\subseteq ℂ$$
9		df-ss	$$⊢S\subseteq ℂ\leftrightarrow S\cap ℂ=S$$
10	8 9	sylib	$$⊢\phi \to S\cap ℂ=S$$
11	2	adantr	$$⊢\left(\phi \wedge x\in ℂ\right)\to A\in ℂ$$
12		0cnd	$$⊢\left(\phi \wedge x\in ℂ\right)\to 0\in ℂ$$
13		dvconst	$$⊢A\in ℂ\to ℂ\mathrm{D}\left(ℂ\times \left\{A\right\}\right)=ℂ\times \left\{0\right\}$$
14	2 13	syl	$$⊢\phi \to ℂ\mathrm{D}\left(ℂ\times \left\{A\right\}\right)=ℂ\times \left\{0\right\}$$
15		fconstmpt	$$⊢ℂ\times \left\{A\right\}=\left(x\in ℂ⟼A\right)$$
16	15	oveq2i	$$⊢ℂ\mathrm{D}\left(ℂ\times \left\{A\right\}\right)=\frac{d\left(x\in ℂ⟼A\right)}{d_{ℂ}x}$$
17		fconstmpt	$$⊢ℂ\times \left\{0\right\}=\left(x\in ℂ⟼0\right)$$
18	14 16 17	3eqtr3g	$$⊢\phi \to \frac{d\left(x\in ℂ⟼A\right)}{d_{ℂ}x}=\left(x\in ℂ⟼0\right)$$
19	3 1 6 10 11 12 18	dvmptres3	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{S}x}=\left(x\in S⟼0\right)$$