This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )