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

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 4 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D F ) <-> x e. X ) )
33 32 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D F ) )
34 1 adantr 
 |-  ( ( ph /\ x e. X ) -> S e. { RR , CC } )
35 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
36 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
37 34 9 35 36 4syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D F ) <-> x ( S _D F ) ( ( S _D F ) ` x ) ) )
38 33 37 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D F ) ( ( S _D F ) ` x ) )
39 5 eleq2d 
 |-  ( ph -> ( x e. dom ( S _D G ) <-> x e. X ) )
40 39 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D G ) )
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 34 14 41 42 4syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. dom ( S _D G ) <-> x ( S _D G ) ( ( S _D G ) ` x ) ) )
44 40 43 mpbid 
 |-  ( ( ph /\ x e. X ) -> x ( S _D G ) ( ( S _D G ) ` x ) )
45 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
46 28 29 30 29 31 38 44 45 dvaddbr 
 |-  ( ( ph /\ x e. X ) -> x ( S _D ( F oF + G ) ) ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) )
47 reldv 
 |-  Rel ( S _D ( F oF + G ) )
48 47 releldmi 
 |-  ( x ( S _D ( F oF + G ) ) ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) -> x e. dom ( S _D ( F oF + G ) ) )
49 46 48 syl 
 |-  ( ( ph /\ x e. X ) -> x e. dom ( S _D ( F oF + G ) ) )
50 27 49 eqelssd 
 |-  ( ph -> dom ( S _D ( F oF + G ) ) = X )
51 50 feq2d 
 |-  ( ph -> ( ( S _D ( F oF + G ) ) : dom ( S _D ( F oF + G ) ) --> CC <-> ( S _D ( F oF + G ) ) : X --> CC ) )
52 20 51 mpbid 
 |-  ( ph -> ( S _D ( F oF + G ) ) : X --> CC )
53 52 ffnd 
 |-  ( ph -> ( S _D ( F oF + G ) ) Fn X )
54 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) = ( ( S _D F ) ` x ) )
55 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) = ( ( S _D G ) ` x ) )
56 28 29 30 29 34 33 40 dvadd 
 |-  ( ( ph /\ x e. X ) -> ( ( S _D ( F oF + G ) ) ` x ) = ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) )
57 56 eqcomd 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) + ( ( S _D G ) ` x ) ) = ( ( S _D ( F oF + G ) ) ` x ) )
58 8 13 18 53 54 55 57 offveq 
 |-  ( ph -> ( ( S _D F ) oF + ( S _D G ) ) = ( S _D ( F oF + G ) ) )
59 58 eqcomd 
 |-  ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) )