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

Metamath Proof Explorer

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