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 ) ) )