Theorem dvmptres

Description: Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
	dvmptres.y	$$⊢\phi \to Y\subseteq X$$
	dvmptres.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
	dvmptres.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvmptres.t	$$⊢\phi \to Y\in J$$
Assertion	dvmptres	$$⊢\phi \to \frac{d\left(x\in Y⟼A\right)}{d_{S}x}=\left(x\in Y⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
3		dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
4		dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
5		dvmptres.y	$$⊢\phi \to Y\subseteq X$$
6		dvmptres.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
7		dvmptres.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8		dvmptres.t	$$⊢\phi \to Y\in J$$
9	7	cnfldtop	$$⊢K\in \mathrm{Top}$$
10		resttop	$$⊢\left(K\in \mathrm{Top}\wedge S\in \left\{ℝ,ℂ\right\}\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
11	9 1 10	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}S\in \mathrm{Top}$$
12	6 11	eqeltrid	$$⊢\phi \to J\in \mathrm{Top}$$
13		isopn3i	$$⊢\left(J\in \mathrm{Top}\wedge Y\in J\right)\to \mathrm{int}\left(J\right)\left(Y\right)=Y$$
14	12 8 13	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(Y\right)=Y$$
15	1 2 3 4 5 6 7 14	dvmptres2	$$⊢\phi \to \frac{d\left(x\in Y⟼A\right)}{d_{S}x}=\left(x\in Y⟼B\right)$$