This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvmptco

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

Ref Expression
Hypotheses dvmptco.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptco.t ⊢ ( 𝜑 → 𝑇 ∈ { ℝ , ℂ } )
dvmptco.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
dvmptco.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptco.c ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐶 ∈ ℂ )
dvmptco.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ 𝑊 )
dvmptco.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptco.dc ⊢ ( 𝜑 → ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) = ( 𝑦 ∈ 𝑌 ↦ 𝐷 ) )
dvmptco.e ⊢ ( 𝑦 = 𝐴 → 𝐶 = 𝐸 )
dvmptco.f ⊢ ( 𝑦 = 𝐴 → 𝐷 = 𝐹 )
Assertion dvmptco ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐸 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptco.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptco.t ⊢ ( 𝜑 → 𝑇 ∈ { ℝ , ℂ } )
3 dvmptco.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
4 dvmptco.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
5 dvmptco.c ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐶 ∈ ℂ )
6 dvmptco.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ 𝑊 )
7 dvmptco.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
8 dvmptco.dc ⊢ ( 𝜑 → ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) = ( 𝑦 ∈ 𝑌 ↦ 𝐷 ) )
9 dvmptco.e ⊢ ( 𝑦 = 𝐴 → 𝐶 = 𝐸 )
10 dvmptco.f ⊢ ( 𝑦 = 𝐴 → 𝐷 = 𝐹 )
11 5 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) : 𝑌 ⟶ ℂ )
12 3 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
13 8 dmeqd ⊢ ( 𝜑 → dom ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) = dom ( 𝑦 ∈ 𝑌 ↦ 𝐷 ) )
14 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 )
15 dmmptg ⊢ ( ∀ 𝑦 ∈ 𝑌 𝐷 ∈ 𝑊 → dom ( 𝑦 ∈ 𝑌 ↦ 𝐷 ) = 𝑌 )
16 14 15 syl ⊢ ( 𝜑 → dom ( 𝑦 ∈ 𝑌 ↦ 𝐷 ) = 𝑌 )
17 13 16 eqtrd ⊢ ( 𝜑 → dom ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) = 𝑌 )
18 7 dmeqd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
19 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
20 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
21 19 20 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
22 18 21 eqtrd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
23 2 1 11 12 17 22 dvcof ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) )
24 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
25 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
26 3 24 25 9 fmptco ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐸 ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐸 ) ) )
28 ovex ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ V
29 28 dmex ⊢ dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ V
30 22 29 eqeltrrdi ⊢ ( 𝜑 → 𝑋 ∈ V )
31 2 5 6 8 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ ℂ )
32 8 31 fmpt3d ⊢ ( 𝜑 → ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) : 𝑌 ⟶ ℂ )
33 fco ⊢ ( ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) : 𝑌 ⟶ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 ) → ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ )
34 32 12 33 syl2anc ⊢ ( 𝜑 → ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ )
35 3 24 8 10 fmptco ⊢ ( 𝜑 → ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐹 ) )
36 35 feq1d ⊢ ( 𝜑 → ( ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐹 ) : 𝑋 ⟶ ℂ ) )
37 34 36 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐹 ) : 𝑋 ⟶ ℂ )
38 37 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ )
39 30 38 4 35 7 offval2 ⊢ ( 𝜑 → ( ( ( 𝑇 D ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · 𝐵 ) ) )
40 23 27 39 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐸 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · 𝐵 ) ) )