Theorem dvbssntr

Description: The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	dvcl.s	$$⊢\phi \to S\subseteq ℂ$$
	dvcl.f	$$⊢\phi \to F:A⟶ℂ$$
	dvcl.a	$$⊢\phi \to A\subseteq S$$
	dvbssntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
	dvbssntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	dvbssntr	$$⊢\phi \to \mathrm{dom}{F}_S^{\prime }\subseteq \mathrm{int}\left(J\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	$$⊢\phi \to S\subseteq ℂ$$
2		dvcl.f	$$⊢\phi \to F:A⟶ℂ$$
3		dvcl.a	$$⊢\phi \to A\subseteq S$$
4		dvbssntr.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
5		dvbssntr.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6	4 5	dvfval	$$⊢\left(S\subseteq ℂ\wedge F:A⟶ℂ\wedge A\subseteq S\right)\to \left(S\mathrm{D}F=\bigcup _{x\in \mathrm{int}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\wedge S\mathrm{D}F\subseteq \mathrm{int}\left(J\right)\left(A\right)\times ℂ\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(S\mathrm{D}F=\bigcup _{x\in \mathrm{int}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(\left(z\in \left(A\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\wedge S\mathrm{D}F\subseteq \mathrm{int}\left(J\right)\left(A\right)\times ℂ\right)$$
8		dmss	$$⊢S\mathrm{D}F\subseteq \mathrm{int}\left(J\right)\left(A\right)\times ℂ\to \mathrm{dom}{F}_S^{\prime }\subseteq \mathrm{dom}\left(\mathrm{int}\left(J\right)\left(A\right)\times ℂ\right)$$
9	7 8	simpl2im	$$⊢\phi \to \mathrm{dom}{F}_S^{\prime }\subseteq \mathrm{dom}\left(\mathrm{int}\left(J\right)\left(A\right)\times ℂ\right)$$
10		dmxpss	$$⊢\mathrm{dom}\left(\mathrm{int}\left(J\right)\left(A\right)\times ℂ\right)\subseteq \mathrm{int}\left(J\right)\left(A\right)$$
11	9 10	sstrdi	$$⊢\phi \to \mathrm{dom}{F}_S^{\prime }\subseteq \mathrm{int}\left(J\right)\left(A\right)$$