dvcof

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

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

Proof

Step	Hyp	Ref	Expression
1		dvcof.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvcof.t	$⊢ φ \to T \in \{ℝ, ℂ\}$
3		dvcof.f	$⊢ φ \to F : X ⟶ ℂ$
4		dvcof.g	$⊢ φ \to G : Y ⟶ X$
5		dvcof.df	$⊢ φ \to dom F_{S}^{'} = X$
6		dvcof.dg	$⊢ φ \to dom G_{T}^{'} = Y$
7	3	adantr	$⊢ (φ \land x \in Y) \to F : X ⟶ ℂ$
8		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
9	5 8	eqsstrrdi	$⊢ φ \to X \subseteq S$
10	9	adantr	$⊢ (φ \land x \in Y) \to X \subseteq S$
11	4	adantr	$⊢ (φ \land x \in Y) \to G : Y ⟶ X$
12		dvbsss	$⊢ dom G_{T}^{'} \subseteq T$
13	6 12	eqsstrrdi	$⊢ φ \to Y \subseteq T$
14	13	adantr	$⊢ (φ \land x \in Y) \to Y \subseteq T$
15	1	adantr	$⊢ (φ \land x \in Y) \to S \in \{ℝ, ℂ\}$
16	2	adantr	$⊢ (φ \land x \in Y) \to T \in \{ℝ, ℂ\}$
17	4	ffvelcdmda	$⊢ (φ \land x \in Y) \to G (x) \in X$
18	5	adantr	$⊢ (φ \land x \in Y) \to dom F_{S}^{'} = X$
19	17 18	eleqtrrd	$⊢ (φ \land x \in Y) \to G (x) \in dom F_{S}^{'}$
20	6	eleq2d	$⊢ φ \to (x \in dom G_{T}^{'} \leftrightarrow x \in Y)$
21	20	biimpar	$⊢ (φ \land x \in Y) \to x \in dom G_{T}^{'}$
22	7 10 11 14 15 16 19 21	dvco	$⊢ (φ \land x \in Y) \to {(F \circ G)}_{T}^{'} (x) = F_{S}^{'} (G (x)) G_{T}^{'} (x)$
23	22	mpteq2dva	$⊢ φ \to (x \in Y ⟼ {(F \circ G)}_{T}^{'} (x)) = (x \in Y ⟼ F_{S}^{'} (G (x)) G_{T}^{'} (x))$
24		dvfg	$⊢ T \in \{ℝ, ℂ\} \to {(F \circ G)}_{T}^{'} : dom {(F \circ G)}_{T}^{'} ⟶ ℂ$
25	2 24	syl	$⊢ φ \to {(F \circ G)}_{T}^{'} : dom {(F \circ G)}_{T}^{'} ⟶ ℂ$
26		recnprss	$⊢ T \in \{ℝ, ℂ\} \to T \subseteq ℂ$
27	2 26	syl	$⊢ φ \to T \subseteq ℂ$
28		fco	$⊢ (F : X ⟶ ℂ \land G : Y ⟶ X) \to (F \circ G) : Y ⟶ ℂ$
29	3 4 28	syl2anc	$⊢ φ \to (F \circ G) : Y ⟶ ℂ$
30	27 29 13	dvbss	$⊢ φ \to dom {(F \circ G)}_{T}^{'} \subseteq Y$
31		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
32	15 31	syl	$⊢ (φ \land x \in Y) \to S \subseteq ℂ$
33	16 26	syl	$⊢ (φ \land x \in Y) \to T \subseteq ℂ$
34		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
35		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
36		funfvbrb	$⊢ Fun F_{S}^{'} \to (G (x) \in dom F_{S}^{'} \leftrightarrow G (x) F_{S}^{'} F_{S}^{'} (G (x)))$
37	15 34 35 36	4syl	$⊢ (φ \land x \in Y) \to (G (x) \in dom F_{S}^{'} \leftrightarrow G (x) F_{S}^{'} F_{S}^{'} (G (x)))$
38	19 37	mpbid	$⊢ (φ \land x \in Y) \to G (x) F_{S}^{'} F_{S}^{'} (G (x))$
39		dvfg	$⊢ T \in \{ℝ, ℂ\} \to G_{T}^{'} : dom G_{T}^{'} ⟶ ℂ$
40		ffun	$⊢ G_{T}^{'} : dom G_{T}^{'} ⟶ ℂ \to Fun G_{T}^{'}$
41		funfvbrb	$⊢ Fun G_{T}^{'} \to (x \in dom G_{T}^{'} \leftrightarrow x G_{T}^{'} G_{T}^{'} (x))$
42	16 39 40 41	4syl	$⊢ (φ \land x \in Y) \to (x \in dom G_{T}^{'} \leftrightarrow x G_{T}^{'} G_{T}^{'} (x))$
43	21 42	mpbid	$⊢ (φ \land x \in Y) \to x G_{T}^{'} G_{T}^{'} (x)$
44		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
45	7 10 11 14 32 33 38 43 44	dvcobr	$⊢ (φ \land x \in Y) \to x {(F \circ G)}_{T}^{'} F_{S}^{'} (G (x)) G_{T}^{'} (x)$
46		reldv	$⊢ Rel {(F \circ G)}_{T}^{'}$
47	46	releldmi	$⊢ x {(F \circ G)}_{T}^{'} F_{S}^{'} (G (x)) G_{T}^{'} (x) \to x \in dom {(F \circ G)}_{T}^{'}$
48	45 47	syl	$⊢ (φ \land x \in Y) \to x \in dom {(F \circ G)}_{T}^{'}$
49	30 48	eqelssd	$⊢ φ \to dom {(F \circ G)}_{T}^{'} = Y$
50	49	feq2d	$⊢ φ \to ({(F \circ G)}_{T}^{'} : dom {(F \circ G)}_{T}^{'} ⟶ ℂ \leftrightarrow {(F \circ G)}_{T}^{'} : Y ⟶ ℂ)$
51	25 50	mpbid	$⊢ φ \to {(F \circ G)}_{T}^{'} : Y ⟶ ℂ$
52	51	feqmptd	$⊢ φ \to T D (F \circ G) = (x \in Y ⟼ {(F \circ G)}_{T}^{'} (x))$
53	2 13	ssexd	$⊢ φ \to Y \in V$
54		fvexd	$⊢ (φ \land x \in Y) \to F_{S}^{'} (G (x)) \in V$
55		fvexd	$⊢ (φ \land x \in Y) \to G_{T}^{'} (x) \in V$
56	4	feqmptd	$⊢ φ \to G = (x \in Y ⟼ G (x))$
57	1 34	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
58	5	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
59	57 58	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
60	59	feqmptd	$⊢ φ \to S D F = (y \in X ⟼ F_{S}^{'} (y))$
61		fveq2	$⊢ y = G (x) \to F_{S}^{'} (y) = F_{S}^{'} (G (x))$
62	17 56 60 61	fmptco	$⊢ φ \to F_{S}^{'} \circ G = (x \in Y ⟼ F_{S}^{'} (G (x)))$
63	2 39	syl	$⊢ φ \to G_{T}^{'} : dom G_{T}^{'} ⟶ ℂ$
64	6	feq2d	$⊢ φ \to (G_{T}^{'} : dom G_{T}^{'} ⟶ ℂ \leftrightarrow G_{T}^{'} : Y ⟶ ℂ)$
65	63 64	mpbid	$⊢ φ \to G_{T}^{'} : Y ⟶ ℂ$
66	65	feqmptd	$⊢ φ \to T D G = (x \in Y ⟼ G_{T}^{'} (x))$
67	53 54 55 62 66	offval2	$⊢ φ \to (F_{S}^{'} \circ G) \times_{f} G_{T}^{'} = (x \in Y ⟼ F_{S}^{'} (G (x)) G_{T}^{'} (x))$
68	23 52 67	3eqtr4d	$⊢ φ \to T D (F \circ G) = (F_{S}^{'} \circ G) \times_{f} G_{T}^{'}$

Metamath Proof Explorer

Theorem dvcof

Proof