Theorem dvmptsub

Description: Function-builder for derivative, subtraction rule. (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 ) )
	dvmptsub.c	|- ( ( ph /\ x e. X ) -> C e. CC )
	dvmptsub.d	|- ( ( ph /\ x e. X ) -> D e. W )
	dvmptsub.dc	|- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
Assertion	dvmptsub	|- ( ph -> ( S _D ( x e. X |-> ( A - C ) ) ) = ( x e. X |-> ( B - D ) ) )

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		dvmptsub.c	|- ( ( ph /\ x e. X ) -> C e. CC )
6		dvmptsub.d	|- ( ( ph /\ x e. X ) -> D e. W )
7		dvmptsub.dc	|- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
8	5	negcld	|- ( ( ph /\ x e. X ) -> -u C e. CC )
9		negex	|- -u D e. _V
10	9	a1i	|- ( ( ph /\ x e. X ) -> -u D e. _V )
11	1 5 6 7	dvmptneg	|- ( ph -> ( S _D ( x e. X |-> -u C ) ) = ( x e. X |-> -u D ) )
12	1 2 3 4 8 10 11	dvmptadd	|- ( ph -> ( S _D ( x e. X |-> ( A + -u C ) ) ) = ( x e. X |-> ( B + -u D ) ) )
13	2 5	negsubd	|- ( ( ph /\ x e. X ) -> ( A + -u C ) = ( A - C ) )
14	13	mpteq2dva	|- ( ph -> ( x e. X |-> ( A + -u C ) ) = ( x e. X |-> ( A - C ) ) )
15	14	oveq2d	|- ( ph -> ( S _D ( x e. X |-> ( A + -u C ) ) ) = ( S _D ( x e. X |-> ( A - C ) ) ) )
16	1 2 3 4	dvmptcl	|- ( ( ph /\ x e. X ) -> B e. CC )
17	1 5 6 7	dvmptcl	|- ( ( ph /\ x e. X ) -> D e. CC )
18	16 17	negsubd	|- ( ( ph /\ x e. X ) -> ( B + -u D ) = ( B - D ) )
19	18	mpteq2dva	|- ( ph -> ( x e. X |-> ( B + -u D ) ) = ( x e. X |-> ( B - D ) ) )
20	12 15 19	3eqtr3d	|- ( ph -> ( S _D ( x e. X |-> ( A - C ) ) ) = ( x e. X |-> ( B - D ) ) )