Metamath Proof Explorer


Theorem dvmul

Description: The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr . (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 dvmul φ F × f G S C = F S C G C + G S C F 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 fvexd φ F S C V
14 fvexd φ G S C V
15 dvfg S F S : dom F S
16 ffun F S : dom F S Fun F S
17 funfvbrb Fun F S C dom F S C F S F S C
18 5 15 16 17 4syl φ C dom F S C F S F S C
19 6 18 mpbid φ C F S F S C
20 dvfg S G S : dom G S
21 ffun G S : dom G S Fun G S
22 funfvbrb Fun G S C dom G S C G S G S C
23 5 20 21 22 4syl φ C dom G S C G S G S C
24 7 23 mpbid φ C G S G S C
25 eqid TopOpen fld = TopOpen fld
26 1 2 3 4 12 13 14 19 24 25 dvmulbr φ C F × f G S F S C G C + G S C F C
27 funbrfv Fun F × f G S C F × f G S F S C G C + G S C F C F × f G S C = F S C G C + G S C F C
28 10 26 27 sylc φ F × f G S C = F S C G C + G S C F C