Theorem dvmptmul

Description: Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvmptadd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvmptadd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvmptadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
	dvmptadd.da	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
	dvmptadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
	dvmptadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
	dvmptadd.dc	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
Assertion	dvmptmul	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvmptadd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3		dvmptadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4		dvmptadd.da	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5		dvmptadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
6		dvmptadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
7		dvmptadd.dc	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
8	2	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
9	5	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) : 𝑋 ⟶ ℂ )
10	4	dmeqd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
11	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
12		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
13	11 12	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
14	10 13	eqtrd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
15	7	dmeqd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
16	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐷 ∈ 𝑊 )
17		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐷 ∈ 𝑊 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = 𝑋 )
18	16 17	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = 𝑋 )
19	15 18	eqtrd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = 𝑋 )
20	1 8 9 14 19	dvmulf	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f + ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) )
21		ovex	⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ V
22	21	dmex	⊢ dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ V
23	19 22	eqeltrrdi	⊢ ( 𝜑 → 𝑋 ∈ V )
24		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
25		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
26	23 2 5 24 25	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) )
27	26	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) )
28		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 · 𝐶 ) ∈ V )
29		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 · 𝐴 ) ∈ V )
30	23 3 5 4 25	offval2	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 · 𝐶 ) ) )
31	23 6 2 7 24	offval2	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 · 𝐴 ) ) )
32	23 28 29 30 31	offval2	⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f + ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )
33	20 27 32	3eqtr3d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )