Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvcof.t	⊢ ( 𝜑 → 𝑇 ∈ { ℝ , ℂ } )
	dvcof.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	dvcof.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
	dvcof.df	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
	dvcof.dg	⊢ ( 𝜑 → dom ( 𝑇 D 𝐺 ) = 𝑌 )
Assertion	dvcof	⊢ ( 𝜑 → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘ 𝐺 ) ∘f · ( 𝑇 D 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvcof.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvcof.t	⊢ ( 𝜑 → 𝑇 ∈ { ℝ , ℂ } )
3		dvcof.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
4		dvcof.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
5		dvcof.df	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
6		dvcof.dg	⊢ ( 𝜑 → dom ( 𝑇 D 𝐺 ) = 𝑌 )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐹 : 𝑋 ⟶ ℂ )
8		dvbsss	⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
9	5 8	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑋 ⊆ 𝑆 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐺 : 𝑌 ⟶ 𝑋 )
12		dvbsss	⊢ dom ( 𝑇 D 𝐺 ) ⊆ 𝑇
13	6 12	eqsstrrdi	⊢ ( 𝜑 → 𝑌 ⊆ 𝑇 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑌 ⊆ 𝑇 )
15	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ { ℝ , ℂ } )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑇 ∈ { ℝ , ℂ } )
17	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑋 )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → dom ( 𝑆 D 𝐹 ) = 𝑋 )
19	17 18	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑥 ) ∈ dom ( 𝑆 D 𝐹 ) )
20	6	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑇 D 𝐺 ) ↔ 𝑥 ∈ 𝑌 ) )
21	20	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom ( 𝑇 D 𝐺 ) )
22	7 10 11 14 15 16 19 21	dvco	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) · ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) )
23	22	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑌 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) · ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) ) )
24		dvfg	⊢ ( 𝑇 ∈ { ℝ , ℂ } → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) : dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ⟶ ℂ )
25	2 24	syl	⊢ ( 𝜑 → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) : dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ⟶ ℂ )
26		recnprss	⊢ ( 𝑇 ∈ { ℝ , ℂ } → 𝑇 ⊆ ℂ )
27	2 26	syl	⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
28		fco	⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) → ( 𝐹 ∘ 𝐺 ) : 𝑌 ⟶ ℂ )
29	3 4 28	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝑌 ⟶ ℂ )
30	27 29 13	dvbss	⊢ ( 𝜑 → dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ⊆ 𝑌 )
31		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
32	15 31	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ⊆ ℂ )
33	16 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑇 ⊆ ℂ )
34		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
35		ffun	⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
36		funfvbrb	⊢ ( Fun ( 𝑆 D 𝐹 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ dom ( 𝑆 D 𝐹 ) ↔ ( 𝐺 ‘ 𝑥 ) ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
37	15 34 35 36	4syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ dom ( 𝑆 D 𝐹 ) ↔ ( 𝐺 ‘ 𝑥 ) ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
38	19 37	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑥 ) ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
39		dvfg	⊢ ( 𝑇 ∈ { ℝ , ℂ } → ( 𝑇 D 𝐺 ) : dom ( 𝑇 D 𝐺 ) ⟶ ℂ )
40		ffun	⊢ ( ( 𝑇 D 𝐺 ) : dom ( 𝑇 D 𝐺 ) ⟶ ℂ → Fun ( 𝑇 D 𝐺 ) )
41		funfvbrb	⊢ ( Fun ( 𝑇 D 𝐺 ) → ( 𝑥 ∈ dom ( 𝑇 D 𝐺 ) ↔ 𝑥 ( 𝑇 D 𝐺 ) ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) )
42	16 39 40 41	4syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ dom ( 𝑇 D 𝐺 ) ↔ 𝑥 ( 𝑇 D 𝐺 ) ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) )
43	21 42	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ( 𝑇 D 𝐺 ) ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) )
44		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
45	7 10 11 14 32 33 38 43 44	dvcobr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) · ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) )
46		reldv	⊢ Rel ( 𝑇 D ( 𝐹 ∘ 𝐺 ) )
47	46	releldmi	⊢ ( 𝑥 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) · ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) → 𝑥 ∈ dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) )
48	45 47	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) )
49	30 48	eqelssd	⊢ ( 𝜑 → dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) = 𝑌 )
50	49	feq2d	⊢ ( 𝜑 → ( ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) : dom ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ⟶ ℂ ↔ ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) : 𝑌 ⟶ ℂ ) )
51	25 50	mpbid	⊢ ( 𝜑 → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) : 𝑌 ⟶ ℂ )
52	51	feqmptd	⊢ ( 𝜑 → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) = ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ‘ 𝑥 ) ) )
53	2 13	ssexd	⊢ ( 𝜑 → 𝑌 ∈ V )
54		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ V )
55		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ∈ V )
56	4	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑥 ) ) )
57	1 34	syl	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
58	5	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
59	57 58	mpbid	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
60	59	feqmptd	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑦 ) ) )
61		fveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑦 ) = ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
62	17 56 60 61	fmptco	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘ 𝐺 ) = ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
63	2 39	syl	⊢ ( 𝜑 → ( 𝑇 D 𝐺 ) : dom ( 𝑇 D 𝐺 ) ⟶ ℂ )
64	6	feq2d	⊢ ( 𝜑 → ( ( 𝑇 D 𝐺 ) : dom ( 𝑇 D 𝐺 ) ⟶ ℂ ↔ ( 𝑇 D 𝐺 ) : 𝑌 ⟶ ℂ ) )
65	63 64	mpbid	⊢ ( 𝜑 → ( 𝑇 D 𝐺 ) : 𝑌 ⟶ ℂ )
66	65	feqmptd	⊢ ( 𝜑 → ( 𝑇 D 𝐺 ) = ( 𝑥 ∈ 𝑌 ↦ ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) )
67	53 54 55 62 66	offval2	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘ 𝐺 ) ∘f · ( 𝑇 D 𝐺 ) ) = ( 𝑥 ∈ 𝑌 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ ( 𝐺 ‘ 𝑥 ) ) · ( ( 𝑇 D 𝐺 ) ‘ 𝑥 ) ) ) )
68	23 52 67	3eqtr4d	⊢ ( 𝜑 → ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) = ( ( ( 𝑆 D 𝐹 ) ∘ 𝐺 ) ∘f · ( 𝑇 D 𝐺 ) ) )