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 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
30 1 29 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
31 30 adantr 
 |-  ( ( ph /\ x e. X ) -> ( S _D F ) : dom ( S _D F ) --> CC )
32 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
33 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
34 31 32 33 3syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
35 13 34 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D F ) ( ( S _D F ) ` x ) )
36 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
37 1 36 syl 
 |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )
38 37 adantr 
 |-  ( ( ph /\ x e. X ) -> ( S _D G ) : dom ( S _D G ) --> CC )
39 ffun 
 |-  ( ( S _D G ) : dom ( S _D G ) --> CC -> Fun ( S _D G ) )
40 funfvbrb 
 |-  ( Fun ( S _D G ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
41 38 39 40 3syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
42 15 41 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D G ) ( ( S _D G ) ` x ) )
43 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
44 6 9 10 9 28 35 42 43 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 ) ) ) )
45 reldv 
 |-  Rel ( S _D ( F oF x. G ) )
46 45 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 ) ) )
47 44 46 syl 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D ( F oF x. G ) ) )
48 27 47 eqelssd 
 |-  ( ph -> dom ( S _D ( F oF x. G ) ) = X )
49 48 feq2d 
 |-  ( ph -> ( ( S _D ( F oF x. G ) ) : dom ( S _D ( F oF x. G ) ) --> CC <-> ( S _D ( F oF x. G ) ) : X --> CC ) )
50 19 49 mpbid 
 |-  ( ph -> ( S _D ( F oF x. G ) ) : X --> CC )
51 50 feqmptd 
 |-  ( ph -> ( S _D ( F oF x. G ) ) = ( x e. X |-> ( ( S _D ( F oF x. G ) ) ` x ) ) )
52 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) e. _V )
53 ovexd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) e. _V )
54 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. _V )
55 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. _V )
56 4 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
57 30 56 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
58 57 feqmptd 
 |-  ( ph -> ( S _D F ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )
59 3 feqmptd 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
60 24 54 55 58 59 offval2 
 |-  ( ph -> ( ( S _D F ) oF x. G ) = ( x e. X |-> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) ) )
61 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) e. _V )
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 37 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 61 62 65 66 offval2 
 |-  ( ph -> ( ( S _D G ) oF x. F ) = ( x e. X |-> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )
68 24 52 53 60 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 51 68 3eqtr4d 
 |-  ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )