Metamath Proof Explorer

Theorem dvmulf

Description: The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvaddf.s 
|- ( ph -> S e. { RR , CC } )
dvaddf.f 
|- ( ph -> F : X --> CC )
dvaddf.g 
|- ( ph -> G : X --> CC )
dvaddf.df 
|- ( ph -> dom ( S _D F ) = X )
dvaddf.dg 
|- ( ph -> dom ( S _D G ) = X )
Assertion dvmulf 
|- ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )

Proof

Step Hyp Ref Expression
1 dvaddf.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvaddf.f 
 |-  ( ph -> F : X --> CC )
3 dvaddf.g 
 |-  ( ph -> G : X --> CC )
4 dvaddf.df 
 |-  ( ph -> dom ( S _D F ) = X )
5 dvaddf.dg 
 |-  ( ph -> dom ( S _D G ) = X )
6 2 adantr 
 |-  ( ( ph /\ x e. X ) -> F : X --> CC )
7 dvbsss 
 |-  dom ( S _D F ) C_ S
8 4 7 eqsstrrdi 
 |-  ( ph -> X C_ S )
9 8 adantr 
 |-  ( ( ph /\ x e. X ) -> X C_ S )
10 3 adantr 
 |-  ( ( ph /\ x e. X ) -> G : X --> CC )
11 1 adantr 
 |-  ( ( ph /\ x e. X ) -> S e. { RR , CC } )
12 4 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D F ) <-> x e. X ) )
13 12 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D F ) )
14 5 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D G ) <-> x e. X ) )
15 14 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D G ) )
16 6 9 10 9 11 13 15 dvmul 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D ( F oF x. G ) ) ` x ) = ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) + ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )
17 16 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( S _D ( F oF x. G ) ) ` x ) ) = ( x e. X |-> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) + ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) ) )
18 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC )
19 1 18 syl 
 |-  ( ph -> ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC )
20 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
21 1 20 syl 
 |-  ( ph -> S C_ CC )
22 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
23 22 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
24 1 8 ssexd 
 |-  ( ph -> X e. _V )
25 inidm 
 |-  ( X i^i X ) = X
26 23 2 3 24 24 25 off 
 |-  ( ph -> ( F oF x. G ) : X --> CC )
27 21 26 8 dvbss 
 |-  ( ph -> dom ( S _D ( F oF x. G ) ) C_ X )
28 21 adantr 
 |-  ( ( ph /\ x e. X ) -> S C_ CC )
29 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. _V )
30 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) e. _V )
31 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
32 1 31 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
33 32 adantr 
 |-  ( ( ph /\ x e. X ) -> ( S _D F ) : dom ( S _D F ) --> CC )
34 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
35 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
36 33 34 35 3syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
37 13 36 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D F ) ( ( S _D F ) ` x ) )
38 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
39 1 38 syl 
 |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )
40 39 adantr 
 |-  ( ( ph /\ x e. X ) -> ( S _D G ) : dom ( S _D G ) --> CC )
41 ffun 
 |-  ( ( S _D G ) : dom ( S _D G ) --> CC -> Fun ( S _D G ) )
42 funfvbrb 
 |-  ( Fun ( S _D G ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
43 40 41 42 3syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
44 15 43 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D G ) ( ( S _D G ) ` x ) )
45 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
46 6 9 10 9 28 29 30 37 44 45 dvmulbr 
 |-  ( ( ph /\ x e. X ) -> x ( S _D ( F oF x. G ) ) ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) + ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )
47 reldv 
 |-  Rel ( S _D ( F oF x. G ) )
48 47 releldmi 
 |-  ( x ( S _D ( F oF x. G ) ) ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) + ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) -> x e. dom ( S _D ( F oF x. G ) ) )
49 46 48 syl 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D ( F oF x. G ) ) )
50 27 49 eqelssd 
 |-  ( ph -> dom ( S _D ( F oF x. G ) ) = X )
51 50 feq2d 
 |-  ( ph -> ( ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC <-> ( S _D ( F oF x. G ) ) : X --> CC ) )
52 19 51 mpbid 
 |-  ( ph -> ( S _D ( F oF x. G ) ) : X --> CC )
53 52 feqmptd 
 |-  ( ph -> ( S _D ( F oF x. G ) ) = ( x e. X |-> ( ( S _D ( F oF x. G ) ) ` x ) ) )
54 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) e. _V )
55 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) e. _V )
56 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. _V )
57 4 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
58 32 57 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
59 58 feqmptd 
 |-  ( ph -> ( S _D F ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )
60 3 feqmptd 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
61 24 29 56 59 60 offval2 
 |-  ( ph -> ( ( S _D F ) oF x. G ) = ( x e. X |-> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) ) )
62 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. _V )
63 5 feq2d 
 |-  ( ph -> ( ( S _D G ) : dom ( S _D G ) --> CC <-> ( S _D G ) : X --> CC ) )
64 39 63 mpbid 
 |-  ( ph -> ( S _D G ) : X --> CC )
65 64 feqmptd 
 |-  ( ph -> ( S _D G ) = ( x e. X |-> ( ( S _D G ) ` x ) ) )
66 2 feqmptd 
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
67 24 30 62 65 66 offval2 
 |-  ( ph -> ( ( S _D G ) oF x. F ) = ( x e. X |-> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )
68 24 54 55 61 67 offval2 
 |-  ( ph -> ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) = ( x e. X |-> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) + ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) ) )
69 17 53 68 3eqtr4d 
 |-  ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )