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

Metamath Proof Explorer

Theorem dvmul

Description: The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvadd.f 
|- ( ph -> F : X --> CC )
dvadd.x 
|- ( ph -> X C_ S )
dvadd.g 
|- ( ph -> G : Y --> CC )
dvadd.y 
|- ( ph -> Y C_ S )
dvadd.s 
|- ( ph -> S e. { RR , CC } )
dvadd.df 
|- ( ph -> C e. dom ( S _D F ) )
dvadd.dg 
|- ( ph -> C e. dom ( S _D G ) )
Assertion dvmul 
|- ( ph -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )

Proof

Step Hyp Ref Expression
1 dvadd.f 
 |-  ( ph -> F : X --> CC )
2 dvadd.x 
 |-  ( ph -> X C_ S )
3 dvadd.g 
 |-  ( ph -> G : Y --> CC )
4 dvadd.y 
 |-  ( ph -> Y C_ S )
5 dvadd.s 
 |-  ( ph -> S e. { RR , CC } )
6 dvadd.df 
 |-  ( ph -> C e. dom ( S _D F ) )
7 dvadd.dg 
 |-  ( ph -> C e. dom ( S _D G ) )
8 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC )
9 ffun 
 |-  ( ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC -> Fun ( S _D ( F oF x. G ) ) )
10 5 8 9 3syl 
 |-  ( ph -> Fun ( S _D ( F oF x. G ) ) )
11 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
12 5 11 syl 
 |-  ( ph -> S C_ CC )
13 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
14 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
15 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
16 5 13 14 15 4syl 
 |-  ( ph -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
17 6 16 mpbid 
 |-  ( ph -> C ( S _D F ) ( ( S _D F ) ` C ) )
18 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
19 ffun 
 |-  ( ( S _D G ) : dom ( S _D G ) --> CC -> Fun ( S _D G ) )
20 funfvbrb 
 |-  ( Fun ( S _D G ) -> ( C e. dom ( S _D G ) <-> C ( S _D G ) ( ( S _D G ) ` C ) ) )
21 5 18 19 20 4syl 
 |-  ( ph -> ( C e. dom ( S _D G ) <-> C ( S _D G ) ( ( S _D G ) ` C ) ) )
22 7 21 mpbid 
 |-  ( ph -> C ( S _D G ) ( ( S _D G ) ` C ) )
23 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
24 1 2 3 4 12 17 22 23 dvmulbr 
 |-  ( ph -> C ( S _D ( F oF x. G ) ) ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )
25 funbrfv 
 |-  ( Fun ( S _D ( F oF x. G ) ) -> ( C ( S _D ( F oF x. G ) ) ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) ) )
26 10 24 25 sylc 
 |-  ( ph -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )