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∈XAdSx=x∈X⟼B
dvmptco.dc ⊢φ→dy∈YCdTy=y∈Y⟼D
dvmptco.e ⊢y=A→C=E
dvmptco.f ⊢y=A→D=F
Assertion dvmptco ⊢φ→dx∈XEdSx=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∈XAdSx=x∈X⟼B
8 dvmptco.dc ⊢φ→dy∈YCdTy=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∈YCdTy=dom⁡y∈Y⟼D
14 6 ralrimiva ⊢φ→∀y∈YD∈W
15 dmmptg ⊢∀y∈YD∈W→dom⁡y∈Y⟼D=Y
16 14 15 syl ⊢φ→dom⁡y∈Y⟼D=Y
17 13 16 eqtrd ⊢φ→dom⁡dy∈YCdTy=Y
18 7 dmeqd ⊢φ→dom⁡dx∈XAdSx=dom⁡x∈X⟼B
19 4 ralrimiva ⊢φ→∀x∈XB∈V
20 dmmptg ⊢∀x∈XB∈V→dom⁡x∈X⟼B=X
21 19 20 syl ⊢φ→dom⁡x∈X⟼B=X
22 18 21 eqtrd ⊢φ→dom⁡dx∈XAdSx=X
23 2 1 11 12 17 22 dvcof ⊢φ→SDy∈Y⟼C∘x∈X⟼A=dy∈YCdTy∘x∈X⟼A×fdx∈XAdSx
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 ⊢φ→SDy∈Y⟼C∘x∈X⟼A=dx∈XEdSx
28 ovex ⊢dx∈XAdSx∈V
29 28 dmex ⊢dom⁡dx∈XAdSx∈V
30 22 29 eqeltrrdi ⊢φ→X∈V
31 2 5 6 8 dvmptcl ⊢φ∧y∈Y→D∈ℂ
32 8 31 fmpt3d ⊢φ→dy∈YCdTy:Y⟶ℂ
33 fco ⊢dy∈YCdTy:Y⟶ℂ∧x∈X⟼A:X⟶Y→dy∈YCdTy∘x∈X⟼A:X⟶ℂ
34 32 12 33 syl2anc ⊢φ→dy∈YCdTy∘x∈X⟼A:X⟶ℂ
35 3 24 8 10 fmptco ⊢φ→dy∈YCdTy∘x∈X⟼A=x∈X⟼F
36 35 feq1d ⊢φ→dy∈YCdTy∘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∈YCdTy∘x∈X⟼A×fdx∈XAdSx=x∈X⟼F⁢B
40 23 27 39 3eqtr3d ⊢φ→dx∈XEdSx=x∈X⟼F⁢B