Theorem dvmptid

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

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

Proof

Step	Hyp	Ref	Expression
1		dvmptid.1	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
4		toponmax	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5	3 4	mp1i	$$⊢\phi \to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
7	1 6	syl	$$⊢\phi \to S\subseteq ℂ$$
8		df-ss	$$⊢S\subseteq ℂ\leftrightarrow S\cap ℂ=S$$
9	7 8	sylib	$$⊢\phi \to S\cap ℂ=S$$
10		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
11		1cnd	$$⊢\left(\phi \wedge x\in ℂ\right)\to 1\in ℂ$$
12		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{ℂ}=\left(x\in ℂ⟼x\right)$$
13	12	eqcomi	$$⊢\left(x\in ℂ⟼x\right)={\mathrm{I}\upharpoonright }_{ℂ}$$
14	13	oveq2i	$$⊢\frac{d\left(x\in ℂ⟼x\right)}{d_{ℂ}x}=ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)$$
15		dvid	$$⊢ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=ℂ\times \left\{1\right\}$$
16		fconstmpt	$$⊢ℂ\times \left\{1\right\}=\left(x\in ℂ⟼1\right)$$
17	14 15 16	3eqtri	$$⊢\frac{d\left(x\in ℂ⟼x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1\right)$$
18	17	a1i	$$⊢\phi \to \frac{d\left(x\in ℂ⟼x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1\right)$$
19	2 1 5 9 10 11 18	dvmptres3	$$⊢\phi \to \frac{d\left(x\in S⟼x\right)}{d_{S}x}=\left(x\in S⟼1\right)$$