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		fvexd	$⊢ φ \to F_{S}^{'} (C) \in V$
14		fvexd	$⊢ φ \to G_{S}^{'} (C) \in V$
15		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
16		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
17		funfvbrb	$⊢ Fun F_{S}^{'} \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
18	5 15 16 17	4syl	$⊢ φ \to (C \in dom F_{S}^{'} \leftrightarrow C F_{S}^{'} F_{S}^{'} (C))$
19	6 18	mpbid	$⊢ φ \to C F_{S}^{'} F_{S}^{'} (C)$
20		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
21		ffun	$⊢ G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \to Fun G_{S}^{'}$
22		funfvbrb	$⊢ Fun G_{S}^{'} \to (C \in dom G_{S}^{'} \leftrightarrow C G_{S}^{'} G_{S}^{'} (C))$
23	5 20 21 22	4syl	$⊢ φ \to (C \in dom G_{S}^{'} \leftrightarrow C G_{S}^{'} G_{S}^{'} (C))$
24	7 23	mpbid	$⊢ φ \to C G_{S}^{'} G_{S}^{'} (C)$
25		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
26	1 2 3 4 12 13 14 19 24 25	dvmulbr	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C))$
27		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))$
28	10 26 27	sylc	$⊢ φ \to {(F \times_{f} G)}_{S}^{'} (C) = F_{S}^{'} (C) G (C) + G_{S}^{'} (C) F (C)$

Metamath Proof Explorer

Theorem dvmul

Proof