Theorem dvmptres

Description: Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptadd.s	|- ( ph -> S e. { RR , CC } )
	dvmptadd.a	|- ( ( ph /\ x e. X ) -> A e. CC )
	dvmptadd.b	|- ( ( ph /\ x e. X ) -> B e. V )
	dvmptadd.da	|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
	dvmptres.y	|- ( ph -> Y C_ X )
	dvmptres.j	|- J = ( K |`t S )
	dvmptres.k	|- K = ( TopOpen ` CCfld )
	dvmptres.t	|- ( ph -> Y e. J )
Assertion	dvmptres	|- ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	|- ( ph -> S e. { RR , CC } )
2		dvmptadd.a	|- ( ( ph /\ x e. X ) -> A e. CC )
3		dvmptadd.b	|- ( ( ph /\ x e. X ) -> B e. V )
4		dvmptadd.da	|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
5		dvmptres.y	|- ( ph -> Y C_ X )
6		dvmptres.j	|- J = ( K |`t S )
7		dvmptres.k	|- K = ( TopOpen ` CCfld )
8		dvmptres.t	|- ( ph -> Y e. J )
9	7	cnfldtop	|- K e. Top
10		resttop	|- ( ( K e. Top /\ S e. { RR , CC } ) -> ( K |`t S ) e. Top )
11	9 1 10	sylancr	|- ( ph -> ( K |`t S ) e. Top )
12	6 11	eqeltrid	|- ( ph -> J e. Top )
13		isopn3i	|- ( ( J e. Top /\ Y e. J ) -> ( ( int ` J ) ` Y ) = Y )
14	12 8 13	syl2anc	|- ( ph -> ( ( int ` J ) ` Y ) = Y )
15	1 2 3 4 5 6 7 14	dvmptres2	|- ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )