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	|- ( ph -> S C_ CC )
	dvcl.f	|- ( ph -> F : A --> CC )
	dvcl.a	|- ( ph -> A C_ S )
	dvbssntr.j	|- J = ( K |`t S )
	dvbssntr.k	|- K = ( TopOpen ` CCfld )
Assertion	dvbssntr	|- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	|- ( ph -> S C_ CC )
2		dvcl.f	|- ( ph -> F : A --> CC )
3		dvcl.a	|- ( ph -> A C_ S )
4		dvbssntr.j	|- J = ( K |`t S )
5		dvbssntr.k	|- K = ( TopOpen ` CCfld )
6	4 5	dvfval	|- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` J ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` J ) ` A ) X. CC ) ) )
7	1 2 3 6	syl3anc	|- ( ph -> ( ( S _D F ) = U_ x e. ( ( int ` J ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` J ) ` A ) X. CC ) ) )
8		dmss	|- ( ( S _D F ) C_ ( ( ( int ` J ) ` A ) X. CC ) -> dom ( S _D F ) C_ dom ( ( ( int ` J ) ` A ) X. CC ) )
9	7 8	simpl2im	|- ( ph -> dom ( S _D F ) C_ dom ( ( ( int ` J ) ` A ) X. CC ) )
10		dmxpss	|- dom ( ( ( int ` J ) ` A ) X. CC ) C_ ( ( int ` J ) ` A )
11	9 10	sstrdi	|- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )