Metamath Proof Explorer

Theorem dvaddf

Description: The sum 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 dvaddf 
|- ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) )

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 dvbsss 
 |-  dom ( S _D F ) C_ S
7 4 6 eqsstrrdi 
 |-  ( ph -> X C_ S )
8 1 7 ssexd 
 |-  ( ph -> X e. _V )
9 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
10 1 9 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
11 4 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
12 10 11 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
13 12 ffnd 
 |-  ( ph -> ( S _D F ) Fn X )
14 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
15 1 14 syl 
 |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )
16 5 feq2d 
 |-  ( ph -> ( ( S _D G ) : dom ( S _D G ) --> CC <-> ( S _D G ) : X --> CC ) )
17 15 16 mpbid 
 |-  ( ph -> ( S _D G ) : X --> CC )
18 17 ffnd 
 |-  ( ph -> ( S _D G ) Fn X )
19 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( F oF + G ) ) : dom ( S _D ( F oF + G ) ) --> CC )
20 1 19 syl 
 |-  ( ph -> ( S _D ( F oF + G ) ) : dom ( S _D ( F oF + G ) ) --> CC )
21 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
22 1 21 syl 
 |-  ( ph -> S C_ CC )
23 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
24 23 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
25 inidm 
 |-  ( X i^i X ) = X
26 24 2 3 8 8 25 off 
 |-  ( ph -> ( F oF + G ) : X --> CC )
27 22 26 7 dvbss 
 |-  ( ph -> dom ( S _D ( F oF + G ) ) C_ X )
28 2 adantr 
 |-  ( ( ph /\ x e. X ) -> F : X --> CC )
29 7 adantr 
 |-  ( ( ph /\ x e. X ) -> X C_ S )
30 3 adantr 
 |-  ( ( ph /\ x e. X ) -> G : X --> CC )
31 22 adantr 
 |-  ( ( ph /\ x e. X ) -> S C_ CC )
32 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. _V )
33 fvexd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) e. _V )
34 4 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D F ) <-> x e. X ) )
35 34 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D F ) )
36 1 adantr 
 |-  ( ( ph /\ x e. X ) -> S e. { RR , CC } )
37 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
38 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
39 36 9 37 38 4syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
40 35 39 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D F ) ( ( S _D F ) ` x ) )
41 5 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D G ) <-> x e. X ) )
42 41 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D G ) )
43 ffun 
 |-  ( ( S _D G ) : dom ( S _D G ) --> CC -> Fun ( S _D G ) )
44 funfvbrb 
 |-  ( Fun ( S _D G ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
45 36 14 43 44 4syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
46 42 45 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D G ) ( ( S _D G ) ` x ) )
47 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
48 28 29 30 29 31 32 33 40 46 47 dvaddbr 
 |-  ( ( ph /\ x e. X ) -> x ( S _D ( F oF + G ) ) ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) )
49 reldv 
 |-  Rel ( S _D ( F oF + G ) )
50 49 releldmi 
 |-  ( x ( S _D ( F oF + G ) ) ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) -> x e. dom ( S _D ( F oF + G ) ) )
51 48 50 syl 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D ( F oF + G ) ) )
52 27 51 eqelssd 
 |-  ( ph -> dom ( S _D ( F oF + G ) ) = X )
53 52 feq2d 
 |-  ( ph -> ( ( S _D ( F oF + G ) ) : dom ( S _D ( F oF + G ) ) --> CC <-> ( S _D ( F oF + G ) ) : X --> CC ) )
54 20 53 mpbid 
 |-  ( ph -> ( S _D ( F oF + G ) ) : X --> CC )
55 54 ffnd 
 |-  ( ph -> ( S _D ( F oF + G ) ) Fn X )
56 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) = ( ( S _D F ) ` x ) )
57 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) = ( ( S _D G ) ` x ) )
58 28 29 30 29 36 35 42 dvadd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D ( F oF + G ) ) ` x ) = ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) )
59 58 eqcomd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) = ( ( S _D ( F oF + G ) ) ` x ) )
60 8 13 18 55 56 57 59 offveq 
 |-  ( ph -> ( ( S _D F ) oF + ( S _D G ) ) = ( S _D ( F oF + G ) ) )
61 60 eqcomd 
 |-  ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) )