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 φ X S
dvadd.g φ G : Y
dvadd.y φ Y S
dvadd.s φ S
dvadd.df φ C dom F S
dvadd.dg φ C dom G S
Assertion dvadd φ F + f G S C = F S C + G S C

Proof

Step Hyp Ref Expression
1 dvadd.f φ F : X
2 dvadd.x φ X S
3 dvadd.g φ G : Y
4 dvadd.y φ Y S
5 dvadd.s φ S
6 dvadd.df φ C dom F S
7 dvadd.dg φ C dom G S
8 dvfg S F + f G S : dom F + f G S
9 ffun F + f G S : dom F + f G S Fun F + f G S
10 5 8 9 3syl φ Fun F + f G S
11 recnprss S S
12 5 11 syl φ S
13 dvfg S F S : dom F S
14 ffun F S : dom F S Fun F S
15 funfvbrb Fun F S C dom F S C F S F S C
16 5 13 14 15 4syl φ C dom F S C F S F S C
17 6 16 mpbid φ C F S F S C
18 dvfg S G S : dom G S
19 ffun G S : dom G S Fun G S
20 funfvbrb Fun G S C dom G S C G S G S C
21 5 18 19 20 4syl φ C dom G S C G S G S C
22 7 21 mpbid φ C G S G S C
23 eqid TopOpen fld = TopOpen fld
24 1 2 3 4 12 17 22 23 dvaddbr φ C F + f G S F S C + G S C
25 funbrfv Fun F + f G S C F + f G S F S C + G S C F + f G S C = F S C + G S C
26 10 24 25 sylc φ F + f G S C = F S C + G S C