Metamath Proof Explorer

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 𝐺 ) ) )