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 fvexd 
 |-  ( ph -> ( ( S _D F ) ` C ) e. _V )
14 fvexd 
 |-  ( ph -> ( ( S _D G ) ` C ) e. _V )
15 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
16 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
17 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
18 5 15 16 17 4syl 
 |-  ( ph -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
19 6 18 mpbid 
 |-  ( ph -> C ( S _D F ) ( ( S _D F ) ` C ) )
20 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
21 ffun 
 |-  ( ( S _D G ) : dom ( S _D G ) --> CC -> Fun ( S _D G ) )
22 funfvbrb 
 |-  ( Fun ( S _D G ) -> ( C e. dom ( S _D G ) <-> C ( S _D G ) ( ( S _D G ) ` C ) ) )
23 5 20 21 22 4syl 
 |-  ( ph -> ( C e. dom ( S _D G ) <-> C ( S _D G ) ( ( S _D G ) ` C ) ) )
24 7 23 mpbid 
 |-  ( ph -> C ( S _D G ) ( ( S _D G ) ` C ) )
25 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
26 1 2 3 4 12 13 14 19 24 25 dvmulbr 
 |-  ( ph -> C ( S _D ( F oF x. G ) ) ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )
27 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 ) ) ) ) )
28 10 26 27 sylc 
 |-  ( ph -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )