Metamath Proof Explorer

Theorem dvmptneg

Description: Function-builder for derivative, product rule for negatives. (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 ) )
Assertion dvmptneg 
|- ( ph -> ( S _D ( x e. X |-> -u A ) ) = ( x e. X |-> -u 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 neg1cn 
 |-  -u 1 e. CC
6 5 a1i 
 |-  ( ph -> -u 1 e. CC )
7 1 2 3 4 6 dvmptcmul 
 |-  ( ph -> ( S _D ( x e. X |-> ( -u 1 x. A ) ) ) = ( x e. X |-> ( -u 1 x. B ) ) )
8 2 mulm1d 
 |-  ( ( ph /\ x e. X ) -> ( -u 1 x. A ) = -u A )
9 8 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( -u 1 x. A ) ) = ( x e. X |-> -u A ) )
10 9 oveq2d 
 |-  ( ph -> ( S _D ( x e. X |-> ( -u 1 x. A ) ) ) = ( S _D ( x e. X |-> -u A ) ) )
11 1 2 3 4 dvmptcl 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
12 11 mulm1d 
 |-  ( ( ph /\ x e. X ) -> ( -u 1 x. B ) = -u B )
13 12 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( -u 1 x. B ) ) = ( x e. X |-> -u B ) )
14 7 10 13 3eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> -u A ) ) = ( x e. X |-> -u B ) )