Metamath Proof Explorer


Theorem dvadd

Description: The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvadd.f φF:X
dvadd.x φXS
dvadd.g φG:Y
dvadd.y φYS
dvadd.s φS
dvadd.df φCdomFS
dvadd.dg φCdomGS
Assertion dvadd φF+fGSC=FSC+GSC

Proof

Step Hyp Ref Expression
1 dvadd.f φF:X
2 dvadd.x φXS
3 dvadd.g φG:Y
4 dvadd.y φYS
5 dvadd.s φS
6 dvadd.df φCdomFS
7 dvadd.dg φCdomGS
8 dvfg SF+fGS:domF+fGS
9 ffun F+fGS:domF+fGSFunF+fGS
10 5 8 9 3syl φFunF+fGS
11 recnprss SS
12 5 11 syl φS
13 dvfg SFS:domFS
14 ffun FS:domFSFunFS
15 funfvbrb FunFSCdomFSCFSFSC
16 5 13 14 15 4syl φCdomFSCFSFSC
17 6 16 mpbid φCFSFSC
18 dvfg SGS:domGS
19 ffun GS:domGSFunGS
20 funfvbrb FunGSCdomGSCGSGSC
21 5 18 19 20 4syl φCdomGSCGSGSC
22 7 21 mpbid φCGSGSC
23 eqid TopOpenfld=TopOpenfld
24 1 2 3 4 12 17 22 23 dvaddbr φCF+fGSFSC+GSC
25 funbrfv FunF+fGSCF+fGSFSC+GSCF+fGSC=FSC+GSC
26 10 24 25 sylc φF+fGSC=FSC+GSC