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

Metamath Proof Explorer

Theorem dvco

Proof