Theorem dvresntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvresntr.s	$$⊢\phi \to S\subseteq ℂ$$
	dvresntr.x	$$⊢\phi \to X\subseteq S$$
	dvresntr.f	$$⊢\phi \to F:X⟶ℂ$$
	dvresntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
	dvresntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvresntr.i	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)=Y$$
Assertion	dvresntr	$$⊢\phi \to S\mathrm{D}F=S\mathrm{D}\left({F\upharpoonright }_Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvresntr.s	$$⊢\phi \to S\subseteq ℂ$$
2		dvresntr.x	$$⊢\phi \to X\subseteq S$$
3		dvresntr.f	$$⊢\phi \to F:X⟶ℂ$$
4		dvresntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
5		dvresntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6		dvresntr.i	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)=Y$$
7	5 4	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge F:X⟶ℂ\right)\wedge \left(X\subseteq S\wedge X\subseteq S\right)\right)\to S\mathrm{D}\left({F\upharpoonright }_X\right)={F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}$$
8	1 3 2 2 7	syl22anc	$$⊢\phi \to S\mathrm{D}\left({F\upharpoonright }_X\right)={F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}$$
9		ffn	$$⊢F:X⟶ℂ\to FFnX$$
10		fnresdm	$$⊢FFnX\to {F\upharpoonright }_X=F$$
11	3 9 10	3syl	$$⊢\phi \to {F\upharpoonright }_X=F$$
12	11	oveq2d	$$⊢\phi \to S\mathrm{D}\left({F\upharpoonright }_X\right)=S\mathrm{D}F$$
13	5	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
14		resttopon	$$⊢\left(K\in \mathrm{TopOn}\left(ℂ\right)\wedge S\subseteq ℂ\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
15	13 1 14	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}S\in \mathrm{TopOn}\left(S\right)$$
16	4 15	eqeltrid	$$⊢\phi \to J\in \mathrm{TopOn}\left(S\right)$$
17		topontop	$$⊢J\in \mathrm{TopOn}\left(S\right)\to J\in \mathrm{Top}$$
18	16 17	syl	$$⊢\phi \to J\in \mathrm{Top}$$
19		toponuni	$$⊢J\in \mathrm{TopOn}\left(S\right)\to S=\bigcup J$$
20	16 19	syl	$$⊢\phi \to S=\bigcup J$$
21	2 20	sseqtrd	$$⊢\phi \to X\subseteq \bigcup J$$
22		eqid	$$⊢\bigcup J=\bigcup J$$
23	22	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)$$
24	18 21 23	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)$$
25	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)$$
26	24 25 6	3eqtr3d	$$⊢\phi \to \mathrm{int}\left(J\right)\left(Y\right)=Y$$
27	26	reseq2d	$$⊢\phi \to {F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}={F_S^{\prime }\upharpoonright }_Y$$
28	22	ntrss2	$$⊢\left(J\in \mathrm{Top}\wedge X\subseteq \bigcup J\right)\to \mathrm{int}\left(J\right)\left(X\right)\subseteq X$$
29	18 21 28	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(X\right)\subseteq X$$
30	6 29	eqsstrrd	$$⊢\phi \to Y\subseteq X$$
31	30 2	sstrd	$$⊢\phi \to Y\subseteq S$$
32	5 4	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge F:X⟶ℂ\right)\wedge \left(X\subseteq S\wedge Y\subseteq S\right)\right)\to S\mathrm{D}\left({F\upharpoonright }_Y\right)={F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}$$
33	1 3 2 31 32	syl22anc	$$⊢\phi \to S\mathrm{D}\left({F\upharpoonright }_Y\right)={F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(Y\right)}$$
34	6	reseq2d	$$⊢\phi \to {F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}={F_S^{\prime }\upharpoonright }_Y$$
35	27 33 34	3eqtr4rd	$$⊢\phi \to {F_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(X\right)}=S\mathrm{D}\left({F\upharpoonright }_Y\right)$$
36	8 12 35	3eqtr3d	$$⊢\phi \to S\mathrm{D}F=S\mathrm{D}\left({F\upharpoonright }_Y\right)$$