Theorem dvmptntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptntr.s	$$⊢\phi \to S\subseteq ℂ$$
	dvmptntr.x	$$⊢\phi \to X\subseteq S$$
	dvmptntr.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
	dvmptntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvmptntr.i	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)=Y$$
Assertion	dvmptntr	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\frac{d\left(x\in Y⟼A\right)}{d_{S}x}$$

Proof

Step	Hyp	Ref	Expression
1		dvmptntr.s	$$⊢\phi \to S\subseteq ℂ$$
2		dvmptntr.x	$$⊢\phi \to X\subseteq S$$
3		dvmptntr.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
4		dvmptntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
5		dvmptntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6		dvmptntr.i	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)=Y$$
7	5	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
8		resttopon	$$⊢\left(K\in \mathrm{TopOn}\left(ℂ\right)\wedge S\subseteq ℂ\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
9	7 1 8	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
10	4 9	eqeltrid	$$⊢\phi \to J\in \mathrm{TopOn}\left(S\right)$$
11		topontop	$$⊢J\in \mathrm{TopOn}\left(S\right)\to J\in \mathrm{Top}$$
12	10 11	syl	$$⊢\phi \to J\in \mathrm{Top}$$
13		toponuni	$$⊢J\in \mathrm{TopOn}\left(S\right)\to S=\bigcup J$$
14	10 13	syl	$$⊢\phi \to S=\bigcup J$$
15	2 14	sseqtrd	$$⊢\phi \to X\subseteq \bigcup J$$
16		eqid	$$⊢\bigcup J=\bigcup J$$
17	16	ntridm	$$⊢\left(J\in \mathrm{Top}\wedge X\subseteq \bigcup J\right)\to \mathrm{int}\left(J\right)\left(\mathrm{int}\left(J\right)\left(X\right)\right)=\mathrm{int}\left(J\right)\left(X\right)$$
18	12 15 17	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(\mathrm{int}\left(J\right)\left(X\right)\right)=\mathrm{int}\left(J\right)\left(X\right)$$
19	6	fveq2d	$$⊢\phi \to \mathrm{int}\left(J\right)\left(\mathrm{int}\left(J\right)\left(X\right)\right)=\mathrm{int}\left(J\right)\left(Y\right)$$
20	18 19	eqtr3d	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)=\mathrm{int}\left(J\right)\left(Y\right)$$
21	20	reseq2d	$$⊢\phi \to {\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}={\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}$$
22	3	fmpttd	$$⊢\phi \to \left(x\in X⟼A\right):X⟶ℂ$$
23	5 4	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge \left(x\in X⟼A\right):X⟶ℂ\right)\wedge \left(X\subseteq S\wedge X\subseteq S\right)\right)\to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)={\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}$$
24	1 22 2 2 23	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)={\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}$$
25	16	ntrss2	$$⊢\left(J\in \mathrm{Top}\wedge X\subseteq \bigcup J\right)\to \mathrm{int}\left(J\right)\left(X\right)\subseteq X$$
26	12 15 25	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)\subseteq X$$
27	6 26	eqsstrrd	$$⊢\phi \to Y\subseteq X$$
28	27 2	sstrd	$$⊢\phi \to Y\subseteq S$$
29	5 4	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge \left(x\in X⟼A\right):X⟶ℂ\right)\wedge \left(X\subseteq S\wedge Y\subseteq S\right)\right)\to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_Y\right)={\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}$$
30	1 22 2 28 29	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_Y\right)={\frac{d\left(x\in X⟼A\right)}{d_{S}x}\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}$$
31	21 24 30	3eqtr4d	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)=S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_Y\right)$$
32		ssid	$$⊢X\subseteq X$$
33		resmpt	$$⊢X\subseteq X\to {\left(x\in X⟼A\right)\upharpoonright }_X=\left(x\in X⟼A\right)$$
34	32 33	mp1i	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_X=\left(x\in X⟼A\right)$$
35	34	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_X\right)=\frac{d\left(x\in X⟼A\right)}{d_{S}x}$$
36	31 35	eqtr3d	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_Y\right)=\frac{d\left(x\in X⟼A\right)}{d_{S}x}$$
37	27	resmptd	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_Y=\left(x\in Y⟼A\right)$$
38	37	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(x\in X⟼A\right)\upharpoonright }_Y\right)=\frac{d\left(x\in Y⟼A\right)}{d_{S}x}$$
39	36 38	eqtr3d	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\frac{d\left(x\in Y⟼A\right)}{d_{S}x}$$