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 ( 𝑥 ∈ 𝑋 ↦ 𝐸 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · 𝐵 ) ) )