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	$⊢ φ \to F : X ⟶ ℂ$
	dvadd.x	$⊢ φ \to X \subseteq S$
	dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
	dvadd.y	$⊢ φ \to Y \subseteq S$
	dvadd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvadd.df	$⊢ φ \to C \in dom F_{S}^{'}$
	dvadd.dg	$⊢ φ \to C \in dom G_{S}^{'}$
Assertion	dvmul	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} (C) = F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C)$

Proof

Step	Hyp	Ref	Expression
1		dvadd.f	$⊢ φ \to F : X ⟶ ℂ$
2		dvadd.x	$⊢ φ \to X \subseteq S$
3		dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
4		dvadd.y	$⊢ φ \to Y \subseteq S$
5		dvadd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
6		dvadd.df	$⊢ φ \to C \in dom F_{S}^{'}$
7		dvadd.dg	$⊢ φ \to C \in dom G_{S}^{'}$
8		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ$
9		ffun	$⊢ {(F \times_{f} G)}_{S}^{'} : dom {(F \times_{f} G)}_{S}^{'} ⟶ ℂ \to Fun {(F \times_{f} G)}_{S}^{'}$
10	5 8 9	3syl	$⊢ φ \to Fun {(F \times_{f} G)}_{S}^{'}$
11		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
12	5 11	syl	$⊢ φ \to S \subseteq ℂ$
13		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
14		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
15		funfvbrb	$⊢ Fun F_{S}^{'} \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
16	5 13 14 15	4syl	$⊢ φ \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
17	6 16	mpbid	$⊢ φ \to C F_{S}^{'} F_{S}^{'} (C)$
18		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
19		ffun	$⊢ G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \to Fun G_{S}^{'}$
20		funfvbrb	$⊢ Fun G_{S}^{'} \to (C \in dom G_{S}^{'} \leftrightarrow C G_{S}^{'} G_{S}^{'} (C))$
21	5 18 19 20	4syl	$⊢ φ \to (C \in dom G_{S}^{'} \leftrightarrow C G_{S}^{'} G_{S}^{'} (C))$
22	7 21	mpbid	$⊢ φ \to C G_{S}^{'} G_{S}^{'} (C)$
23		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
24	1 2 3 4 12 17 22 23	dvmulbr	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C))$
25		funbrfv	$⊢ Fun {(F \times_{f} G)}_{S}^{'} \to (C {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C)) \to {(F \times_{f} G)}_{S}^{'} (C) = F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C))$
26	10 24 25	sylc	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} (C) = F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C)$

Metamath Proof Explorer

Theorem dvmul

Proof