Theorem dvmptres3

Description: Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptres3.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvmptres3.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptres3.x	$$⊢\phi \to X\in J$$
	dvmptres3.y	$$⊢\phi \to S\cap X=Y$$
	dvmptres3.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptres3.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptres3.d	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}=\left(x\in X⟼B\right)$$
Assertion	dvmptres3	$$⊢\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		dvmptres3.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		dvmptres3.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
3		dvmptres3.x	$$⊢\phi \to X\in J$$
4		dvmptres3.y	$$⊢\phi \to S\cap X=Y$$
5		dvmptres3.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
6		dvmptres3.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
7		dvmptres3.d	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}=\left(x\in X⟼B\right)$$
8	5	fmpttd	$$⊢\phi \to \left(x\in X⟼A\right):X⟶ℂ$$
9	7	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}=\mathrm{dom}\left(x\in X⟼B\right)$$
10		eqid	$$⊢\left(x\in X⟼B\right)=\left(x\in X⟼B\right)$$
11	10 6	dmmptd	$$⊢\phi \to \mathrm{dom}\left(x\in X⟼B\right)=X$$
12	9 11	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}=X$$
13	1	dvres3a	$$⊢\left(\left(S\in \left\{ℝ,ℂ\right\}\wedge \left(x\in X⟼A\right):X⟶ℂ\right)\wedge \left(X\in J\wedge \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}=X\right)\right)\to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_S\right)={\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}\upharpoonright }_S$$
14	2 8 3 12 13	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_S\right)={\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}\upharpoonright }_S$$
15		rescom	$$⊢{\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)\upharpoonright }_S={\left({\left(x\in X⟼A\right)\upharpoonright }_S\right)\upharpoonright }_X$$
16		resres	$$⊢{\left({\left(x\in X⟼A\right)\upharpoonright }_S\right)\upharpoonright }_X={\left(x\in X⟼A\right)\upharpoonright }_{\left(S\cap X\right)}$$
17	15 16	eqtri	$$⊢{\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)\upharpoonright }_S={\left(x\in X⟼A\right)\upharpoonright }_{\left(S\cap X\right)}$$
18	4	reseq2d	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_{\left(S\cap X\right)}={\left(x\in X⟼A\right)\upharpoonright }_Y$$
19	17 18	syl5eq	$$⊢\phi \to {\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)\upharpoonright }_S={\left(x\in X⟼A\right)\upharpoonright }_Y$$
20		ffn	$$⊢\left(x\in X⟼A\right):X⟶ℂ\to \left(x\in X⟼A\right)FnX$$
21		fnresdm	$$⊢\left(x\in X⟼A\right)FnX\to {\left(x\in X⟼A\right)\upharpoonright }_X=\left(x\in X⟼A\right)$$
22	8 20 21	3syl	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_X=\left(x\in X⟼A\right)$$
23	22	reseq1d	$$⊢\phi \to {\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)\upharpoonright }_S={\left(x\in X⟼A\right)\upharpoonright }_S$$
24		inss2	$$⊢S\cap X\subseteq X$$
25	4 24	eqsstrrdi	$$⊢\phi \to Y\subseteq X$$
26	25	resmptd	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_Y=\left(x\in Y⟼A\right)$$
27	19 23 26	3eqtr3d	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_S=\left(x\in Y⟼A\right)$$
28	27	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_S\right)=\frac{d\left(x\in Y⟼A\right)}{d_{S}x}$$
29		rescom	$$⊢{\left({\left(x\in X⟼B\right)\upharpoonright }_X\right)\upharpoonright }_S={\left({\left(x\in X⟼B\right)\upharpoonright }_S\right)\upharpoonright }_X$$
30		resres	$$⊢{\left({\left(x\in X⟼B\right)\upharpoonright }_S\right)\upharpoonright }_X={\left(x\in X⟼B\right)\upharpoonright }_{\left(S\cap X\right)}$$
31	29 30	eqtri	$$⊢{\left({\left(x\in X⟼B\right)\upharpoonright }_X\right)\upharpoonright }_S={\left(x\in X⟼B\right)\upharpoonright }_{\left(S\cap X\right)}$$
32	4	reseq2d	$$⊢\phi \to {\left(x\in X⟼B\right)\upharpoonright }_{\left(S\cap X\right)}={\left(x\in X⟼B\right)\upharpoonright }_Y$$
33	31 32	syl5eq	$$⊢\phi \to {\left({\left(x\in X⟼B\right)\upharpoonright }_X\right)\upharpoonright }_S={\left(x\in X⟼B\right)\upharpoonright }_Y$$
34	6	ralrimiva	$$⊢\phi \to \forall x\in XB\in V$$
35	10	fnmpt	$$⊢\forall x\in XB\in V\to \left(x\in X⟼B\right)FnX$$
36		fnresdm	$$⊢\left(x\in X⟼B\right)FnX\to {\left(x\in X⟼B\right)\upharpoonright }_X=\left(x\in X⟼B\right)$$
37	34 35 36	3syl	$$⊢\phi \to {\left(x\in X⟼B\right)\upharpoonright }_X=\left(x\in X⟼B\right)$$
38	37 7	eqtr4d	$$⊢\phi \to {\left(x\in X⟼B\right)\upharpoonright }_X=\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}$$
39	38	reseq1d	$$⊢\phi \to {\left({\left(x\in X⟼B\right)\upharpoonright }_X\right)\upharpoonright }_S={\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}\upharpoonright }_S$$
40	25	resmptd	$$⊢\phi \to {\left(x\in X⟼B\right)\upharpoonright }_Y=\left(x\in Y⟼B\right)$$
41	33 39 40	3eqtr3d	$$⊢\phi \to {\frac{d\left(x\in X⟼A\right)}{d_{ℂ}x}\upharpoonright }_S=\left(x\in Y⟼B\right)$$
42	14 28 41	3eqtr3d	$$⊢\phi \to \frac{d\left(x\in Y⟼A\right)}{d_{S}x}=\left(x\in Y⟼B\right)$$