# Metamath Proof Explorer

## Theorem dvmulf

Description: The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvaddf.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvaddf.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
dvaddf.g ${⊢}{\phi }\to {G}:{X}⟶ℂ$
dvaddf.df ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
dvaddf.dg ${⊢}{\phi }\to \mathrm{dom}{{G}}_{{S}}^{\prime }={X}$
Assertion dvmulf ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{×}_{f}{G}\right)=\left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){+}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)$

### Proof

Step Hyp Ref Expression
1 dvaddf.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvaddf.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
3 dvaddf.g ${⊢}{\phi }\to {G}:{X}⟶ℂ$
4 dvaddf.df ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
5 dvaddf.dg ${⊢}{\phi }\to \mathrm{dom}{{G}}_{{S}}^{\prime }={X}$
6 2 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}:{X}⟶ℂ$
7 dvbsss ${⊢}\mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
8 4 7 eqsstrrdi ${⊢}{\phi }\to {X}\subseteq {S}$
9 8 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {X}\subseteq {S}$
10 3 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {G}:{X}⟶ℂ$
11 1 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {S}\in \left\{ℝ,ℂ\right\}$
12 4 eleq2d ${⊢}{\phi }\to \left({x}\in \mathrm{dom}{{F}}_{{S}}^{\prime }↔{x}\in {X}\right)$
13 12 biimpar ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in \mathrm{dom}{{F}}_{{S}}^{\prime }$
14 5 eleq2d ${⊢}{\phi }\to \left({x}\in \mathrm{dom}{{G}}_{{S}}^{\prime }↔{x}\in {X}\right)$
15 14 biimpar ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in \mathrm{dom}{{G}}_{{S}}^{\prime }$
16 6 9 10 9 11 13 15 dvmul ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\left({x}\right)={{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)+{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)$
17 16 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\left({x}\right)\right)=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)+{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
18 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }:\mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }⟶ℂ$
19 1 18 syl ${⊢}{\phi }\to {\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }:\mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }⟶ℂ$
20 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
21 1 20 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
22 mulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}{y}\in ℂ$
23 22 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}{y}\in ℂ$
24 1 8 ssexd ${⊢}{\phi }\to {X}\in \mathrm{V}$
25 inidm ${⊢}{X}\cap {X}={X}$
26 23 2 3 24 24 25 off ${⊢}{\phi }\to \left({F}{×}_{f}{G}\right):{X}⟶ℂ$
27 21 26 8 dvbss ${⊢}{\phi }\to \mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\subseteq {X}$
28 21 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {S}\subseteq ℂ$
29 fvexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right)\in \mathrm{V}$
30 fvexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}}_{{S}}^{\prime }\left({x}\right)\in \mathrm{V}$
31 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
32 1 31 syl ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
33 32 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
34 ffun ${⊢}{{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ\to \mathrm{Fun}{{F}}_{{S}}^{\prime }$
35 funfvbrb ${⊢}\mathrm{Fun}{{F}}_{{S}}^{\prime }\to \left({x}\in \mathrm{dom}{{F}}_{{S}}^{\prime }↔{x}{{F}}_{{S}}^{\prime }{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
36 33 34 35 3syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in \mathrm{dom}{{F}}_{{S}}^{\prime }↔{x}{{F}}_{{S}}^{\prime }{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
37 13 36 mpbid ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}{{F}}_{{S}}^{\prime }{{F}}_{{S}}^{\prime }\left({x}\right)$
38 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ$
39 1 38 syl ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ$
40 39 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ$
41 ffun ${⊢}{{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ\to \mathrm{Fun}{{G}}_{{S}}^{\prime }$
42 funfvbrb ${⊢}\mathrm{Fun}{{G}}_{{S}}^{\prime }\to \left({x}\in \mathrm{dom}{{G}}_{{S}}^{\prime }↔{x}{{G}}_{{S}}^{\prime }{{G}}_{{S}}^{\prime }\left({x}\right)\right)$
43 40 41 42 3syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in \mathrm{dom}{{G}}_{{S}}^{\prime }↔{x}{{G}}_{{S}}^{\prime }{{G}}_{{S}}^{\prime }\left({x}\right)\right)$
44 15 43 mpbid ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}{{G}}_{{S}}^{\prime }{{G}}_{{S}}^{\prime }\left({x}\right)$
45 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
46 6 9 10 9 28 29 30 37 44 45 dvmulbr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\left({{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)+{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
47 reldv ${⊢}\mathrm{Rel}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }$
48 47 releldmi ${⊢}{x}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\left({{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)+{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)\to {x}\in \mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }$
49 46 48 syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in \mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }$
50 27 49 eqelssd ${⊢}{\phi }\to \mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }={X}$
51 50 feq2d ${⊢}{\phi }\to \left({\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }:\mathrm{dom}{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }⟶ℂ↔{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }:{X}⟶ℂ\right)$
52 19 51 mpbid ${⊢}{\phi }\to {\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }:{X}⟶ℂ$
53 52 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{×}_{f}{G}\right)=\left({x}\in {X}⟼{\left({F}{×}_{f}{G}\right)}_{{S}}^{\prime }\left({x}\right)\right)$
54 ovexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)\in \mathrm{V}$
55 ovexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\in \mathrm{V}$
56 fvexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {G}\left({x}\right)\in \mathrm{V}$
57 4 feq2d ${⊢}{\phi }\to \left({{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ↔{{F}}_{{S}}^{\prime }:{X}⟶ℂ\right)$
58 32 57 mpbid ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:{X}⟶ℂ$
59 58 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}{F}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
60 3 feqmptd ${⊢}{\phi }\to {G}=\left({x}\in {X}⟼{G}\left({x}\right)\right)$
61 24 29 56 59 60 offval2 ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }{×}_{f}{G}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)\right)$
62 fvexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in \mathrm{V}$
63 5 feq2d ${⊢}{\phi }\to \left({{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ↔{{G}}_{{S}}^{\prime }:{X}⟶ℂ\right)$
64 39 63 mpbid ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }:{X}⟶ℂ$
65 64 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}{G}=\left({x}\in {X}⟼{{G}}_{{S}}^{\prime }\left({x}\right)\right)$
66 2 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {X}⟼{F}\left({x}\right)\right)$
67 24 30 62 65 66 offval2 ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }{×}_{f}{F}=\left({x}\in {X}⟼{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
68 24 54 55 61 67 offval2 ${⊢}{\phi }\to \left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){+}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)+{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
69 17 53 68 3eqtr4d ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{×}_{f}{G}\right)=\left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){+}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)$