dvco

Description: The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Hypotheses	dvco.f	$⊢ φ \to F : X ⟶ ℂ$
	dvco.x	$⊢ φ \to X \subseteq S$
	dvco.g	$⊢ φ \to G : Y ⟶ X$
	dvco.y	$⊢ φ \to Y \subseteq T$
	dvco.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvco.t	$⊢ φ \to T \in \{ℝ, ℂ\}$
	dvco.df	$⊢ φ \to G (C) \in dom F_{S}^{'}$
	dvco.dg	$⊢ φ \to C \in dom G_{T}^{'}$
Assertion	dvco	$⊢ φ \to {(F \circ G)}_{T}^{'} (C) = F_{S}^{'} (G (C)) G_{T}^{'} (C)$

Proof

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

Metamath Proof Explorer

Theorem dvco

Proof