Metamath Proof Explorer

Theorem dvmptmul

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

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 dvmptadd.c 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
6 dvmptadd.d 
 |-  ( ( ph /\ x e. X ) -> D e. W )
7 dvmptadd.dc 
 |-  ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
8 2 fmpttd 
 |-  ( ph -> ( x e. X |-> A ) : X --> CC )
9 5 fmpttd 
 |-  ( ph -> ( x e. X |-> C ) : X --> CC )
10 4 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
11 3 ralrimiva 
 |-  ( ph -> A. x e. X B e. V )
12 dmmptg 
 |-  ( A. x e. X B e. V -> dom ( x e. X |-> B ) = X )
13 11 12 syl 
 |-  ( ph -> dom ( x e. X |-> B ) = X )
14 10 13 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = X )
15 7 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> C ) ) = dom ( x e. X |-> D ) )
16 6 ralrimiva 
 |-  ( ph -> A. x e. X D e. W )
17 dmmptg 
 |-  ( A. x e. X D e. W -> dom ( x e. X |-> D ) = X )
18 16 17 syl 
 |-  ( ph -> dom ( x e. X |-> D ) = X )
19 15 18 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> C ) ) = X )
20 1 8 9 14 19 dvmulf 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) oF x. ( x e. X |-> C ) ) ) = ( ( ( S _D ( x e. X |-> A ) ) oF x. ( x e. X |-> C ) ) oF + ( ( S _D ( x e. X |-> C ) ) oF x. ( x e. X |-> A ) ) ) )
21 ovex 
 |-  ( S _D ( x e. X |-> C ) ) e. _V
22 21 dmex 
 |-  dom ( S _D ( x e. X |-> C ) ) e. _V
23 19 22 eqeltrrdi 
 |-  ( ph -> X e. _V )
24 eqidd 
 |-  ( ph -> ( x e. X |-> A ) = ( x e. X |-> A ) )
25 eqidd 
 |-  ( ph -> ( x e. X |-> C ) = ( x e. X |-> C ) )
26 23 2 5 24 25 offval2 
 |-  ( ph -> ( ( x e. X |-> A ) oF x. ( x e. X |-> C ) ) = ( x e. X |-> ( A x. C ) ) )
27 26 oveq2d 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) oF x. ( x e. X |-> C ) ) ) = ( S _D ( x e. X |-> ( A x. C ) ) ) )
28 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( B x. C ) e. _V )
29 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( D x. A ) e. _V )
30 23 3 5 4 25 offval2 
 |-  ( ph -> ( ( S _D ( x e. X |-> A ) ) oF x. ( x e. X |-> C ) ) = ( x e. X |-> ( B x. C ) ) )
31 23 6 2 7 24 offval2 
 |-  ( ph -> ( ( S _D ( x e. X |-> C ) ) oF x. ( x e. X |-> A ) ) = ( x e. X |-> ( D x. A ) ) )
32 23 28 29 30 31 offval2 
 |-  ( ph -> ( ( ( S _D ( x e. X |-> A ) ) oF x. ( x e. X |-> C ) ) oF + ( ( S _D ( x e. X |-> C ) ) oF x. ( x e. X |-> A ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )
33 20 27 32 3eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )