Metamath Proof Explorer

Theorem dvmptco

Description: Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses dvmptco.s ⊢ φ → S ∈ ℝ ℂ
dvmptco.t ⊢ φ → T ∈ ℝ ℂ
dvmptco.a ⊢ φ ∧ x ∈ X → A ∈ Y
dvmptco.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptco.c ⊢ φ ∧ y ∈ Y → C ∈ ℂ
dvmptco.d ⊢ φ ∧ y ∈ Y → D ∈ W
dvmptco.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
dvmptco.dc ⊢ φ → dy ∈ Y C dT y = y ∈ Y ⟼ D
dvmptco.e ⊢ y = A → C = E
dvmptco.f ⊢ y = A → D = F
Assertion dvmptco ⊢ φ → dx ∈ X E dS x = x ∈ X ⟼ F ⁢ B

Proof

Step Hyp Ref Expression
1 dvmptco.s ⊢ φ → S ∈ ℝ ℂ
2 dvmptco.t ⊢ φ → T ∈ ℝ ℂ
3 dvmptco.a ⊢ φ ∧ x ∈ X → A ∈ Y
4 dvmptco.b ⊢ φ ∧ x ∈ X → B ∈ V
5 dvmptco.c ⊢ φ ∧ y ∈ Y → C ∈ ℂ
6 dvmptco.d ⊢ φ ∧ y ∈ Y → D ∈ W
7 dvmptco.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
8 dvmptco.dc ⊢ φ → dy ∈ Y C dT y = y ∈ Y ⟼ D
9 dvmptco.e ⊢ y = A → C = E
10 dvmptco.f ⊢ y = A → D = F
11 5 fmpttd ⊢ φ → y ∈ Y ⟼ C : Y ⟶ ℂ
12 3 fmpttd ⊢ φ → x ∈ X ⟼ A : X ⟶ Y
13 8 dmeqd ⊢ φ → dom ⁡ dy ∈ Y C dT y = dom ⁡ y ∈ Y ⟼ D
14 6 ralrimiva ⊢ φ → ∀ y ∈ Y D ∈ W
15 dmmptg ⊢ ∀ y ∈ Y D ∈ W → dom ⁡ y ∈ Y ⟼ D = Y
16 14 15 syl ⊢ φ → dom ⁡ y ∈ Y ⟼ D = Y
17 13 16 eqtrd ⊢ φ → dom ⁡ dy ∈ Y C dT y = Y
18 7 dmeqd ⊢ φ → dom ⁡ dx ∈ X A dS x = dom ⁡ x ∈ X ⟼ B
19 4 ralrimiva ⊢ φ → ∀ x ∈ X B ∈ V
20 dmmptg ⊢ ∀ x ∈ X B ∈ V → dom ⁡ x ∈ X ⟼ B = X
21 19 20 syl ⊢ φ → dom ⁡ x ∈ X ⟼ B = X
22 18 21 eqtrd ⊢ φ → dom ⁡ dx ∈ X A dS x = X
23 2 1 11 12 17 22 dvcof ⊢ φ → S D y ∈ Y ⟼ C ∘ x ∈ X ⟼ A = dy ∈ Y C dT y ∘ x ∈ X ⟼ A × f dx ∈ X A dS x
24 eqidd ⊢ φ → x ∈ X ⟼ A = x ∈ X ⟼ A
25 eqidd ⊢ φ → y ∈ Y ⟼ C = y ∈ Y ⟼ C
26 3 24 25 9 fmptco ⊢ φ → y ∈ Y ⟼ C ∘ x ∈ X ⟼ A = x ∈ X ⟼ E
27 26 oveq2d ⊢ φ → S D y ∈ Y ⟼ C ∘ x ∈ X ⟼ A = dx ∈ X E dS x
28 ovex ⊢ dx ∈ X A dS x ∈ V
29 28 dmex ⊢ dom ⁡ dx ∈ X A dS x ∈ V
30 22 29 eqeltrrdi ⊢ φ → X ∈ V
31 2 5 6 8 dvmptcl ⊢ φ ∧ y ∈ Y → D ∈ ℂ
32 8 31 fmpt3d ⊢ φ → dy ∈ Y C dT y : Y ⟶ ℂ
33 fco ⊢ dy ∈ Y C dT y : Y ⟶ ℂ ∧ x ∈ X ⟼ A : X ⟶ Y → dy ∈ Y C dT y ∘ x ∈ X ⟼ A : X ⟶ ℂ
34 32 12 33 syl2anc ⊢ φ → dy ∈ Y C dT y ∘ x ∈ X ⟼ A : X ⟶ ℂ
35 3 24 8 10 fmptco ⊢ φ → dy ∈ Y C dT y ∘ x ∈ X ⟼ A = x ∈ X ⟼ F
36 35 feq1d ⊢ φ → dy ∈ Y C dT y ∘ x ∈ X ⟼ A : X ⟶ ℂ ↔ x ∈ X ⟼ F : X ⟶ ℂ
37 34 36 mpbid ⊢ φ → x ∈ X ⟼ F : X ⟶ ℂ
38 37 fvmptelcdm ⊢ φ ∧ x ∈ X → F ∈ ℂ
39 30 38 4 35 7 offval2 ⊢ φ → dy ∈ Y C dT y ∘ x ∈ X ⟼ A × f dx ∈ X A dS x = x ∈ X ⟼ F ⁢ B
40 23 27 39 3eqtr3d ⊢ φ → dx ∈ X E dS x = x ∈ X ⟼ F ⁢ B