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

Metamath Proof Explorer

Theorem dvmptadd

Description: Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s 
|- ( ph -> S e. { RR , CC } )
dvmptadd.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptadd.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptadd.da 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
dvmptadd.c 
|- ( ( ph /\ x e. X ) -> C e. CC )
dvmptadd.d 
|- ( ( ph /\ x e. X ) -> D e. W )
dvmptadd.dc 
|- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
Assertion dvmptadd 
|- ( ph -> ( S _D ( x e. X |-> ( A + C ) ) ) = ( x e. X |-> ( B + D ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptadd.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
3 dvmptadd.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
4 dvmptadd.da 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
5 dvmptadd.c 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
6 dvmptadd.d 
 |-  ( ( ph /\ x e. X ) -> D e. W )
7 dvmptadd.dc 
 |-  ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )
8 2 fmpttd 
 |-  ( ph -> ( x e. X |-> A ) : X --> CC )
9 5 fmpttd 
 |-  ( ph -> ( x e. X |-> C ) : X --> CC )
10 4 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
11 3 ralrimiva 
 |-  ( ph -> A. x e. X B e. V )
12 dmmptg 
 |-  ( A. x e. X B e. V -> dom ( x e. X |-> B ) = X )
13 11 12 syl 
 |-  ( ph -> dom ( x e. X |-> B ) = X )
14 10 13 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = X )
15 7 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> C ) ) = dom ( x e. X |-> D ) )
16 6 ralrimiva 
 |-  ( ph -> A. x e. X D e. W )
17 dmmptg 
 |-  ( A. x e. X D e. W -> dom ( x e. X |-> D ) = X )
18 16 17 syl 
 |-  ( ph -> dom ( x e. X |-> D ) = X )
19 15 18 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> C ) ) = X )
20 1 8 9 14 19 dvaddf 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) oF + ( x e. X |-> C ) ) ) = ( ( S _D ( x e. X |-> A ) ) oF + ( S _D ( x e. X |-> C ) ) ) )
21 ovex 
 |-  ( S _D ( x e. X |-> C ) ) e. _V
22 21 dmex 
 |-  dom ( S _D ( x e. X |-> C ) ) e. _V
23 19 22 eqeltrrdi 
 |-  ( ph -> X e. _V )
24 eqidd 
 |-  ( ph -> ( x e. X |-> A ) = ( x e. X |-> A ) )
25 eqidd 
 |-  ( ph -> ( x e. X |-> C ) = ( x e. X |-> C ) )
26 23 2 5 24 25 offval2 
 |-  ( ph -> ( ( x e. X |-> A ) oF + ( x e. X |-> C ) ) = ( x e. X |-> ( A + C ) ) )
27 26 oveq2d 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) oF + ( x e. X |-> C ) ) ) = ( S _D ( x e. X |-> ( A + C ) ) ) )
28 23 3 6 4 7 offval2 
 |-  ( ph -> ( ( S _D ( x e. X |-> A ) ) oF + ( S _D ( x e. X |-> C ) ) ) = ( x e. X |-> ( B + D ) ) )
29 20 27 28 3eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> ( A + C ) ) ) = ( x e. X |-> ( B + D ) ) )