Metamath Proof Explorer

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 ⊢φ→S∈ℝℂ
dvmptadd.a ⊢φ∧x∈X→A∈ℂ
dvmptadd.b ⊢φ∧x∈X→B∈V
dvmptadd.da ⊢φ→dx∈XAdSx=x∈X⟼B
dvmptadd.c ⊢φ∧x∈X→C∈ℂ
dvmptadd.d ⊢φ∧x∈X→D∈W
dvmptadd.dc ⊢φ→dx∈XCdSx=x∈X⟼D
Assertion dvmptmul ⊢φ→dx∈XA⁢CdSx=x∈X⟼B⁢C+D⁢A

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢φ→S∈ℝℂ
2 dvmptadd.a ⊢φ∧x∈X→A∈ℂ
3 dvmptadd.b ⊢φ∧x∈X→B∈V
4 dvmptadd.da ⊢φ→dx∈XAdSx=x∈X⟼B
5 dvmptadd.c ⊢φ∧x∈X→C∈ℂ
6 dvmptadd.d ⊢φ∧x∈X→D∈W
7 dvmptadd.dc ⊢φ→dx∈XCdSx=x∈X⟼D
8 2 fmpttd ⊢φ→x∈X⟼A:X⟶ℂ
9 5 fmpttd ⊢φ→x∈X⟼C:X⟶ℂ
10 4 dmeqd ⊢φ→dom⁡dx∈XAdSx=dom⁡x∈X⟼B
11 3 ralrimiva ⊢φ→∀x∈XB∈V
12 dmmptg ⊢∀x∈XB∈V→dom⁡x∈X⟼B=X
13 11 12 syl ⊢φ→dom⁡x∈X⟼B=X
14 10 13 eqtrd ⊢φ→dom⁡dx∈XAdSx=X
15 7 dmeqd ⊢φ→dom⁡dx∈XCdSx=dom⁡x∈X⟼D
16 6 ralrimiva ⊢φ→∀x∈XD∈W
17 dmmptg ⊢∀x∈XD∈W→dom⁡x∈X⟼D=X
18 16 17 syl ⊢φ→dom⁡x∈X⟼D=X
19 15 18 eqtrd ⊢φ→dom⁡dx∈XCdSx=X
20 1 8 9 14 19 dvmulf ⊢φ→SDx∈X⟼A×fx∈X⟼C=dx∈XAdSx×fx∈X⟼C+fdx∈XCdSx×fx∈X⟼A
21 ovex ⊢dx∈XCdSx∈V
22 21 dmex ⊢dom⁡dx∈XCdSx∈V
23 19 22 eqeltrrdi ⊢φ→X∈V
24 eqidd ⊢φ→x∈X⟼A=x∈X⟼A
25 eqidd ⊢φ→x∈X⟼C=x∈X⟼C
26 23 2 5 24 25 offval2 ⊢φ→x∈X⟼A×fx∈X⟼C=x∈X⟼A⁢C
27 26 oveq2d ⊢φ→SDx∈X⟼A×fx∈X⟼C=dx∈XA⁢CdSx
28 ovexd ⊢φ∧x∈X→B⁢C∈V
29 ovexd ⊢φ∧x∈X→D⁢A∈V
30 23 3 5 4 25 offval2 ⊢φ→dx∈XAdSx×fx∈X⟼C=x∈X⟼B⁢C
31 23 6 2 7 24 offval2 ⊢φ→dx∈XCdSx×fx∈X⟼A=x∈X⟼D⁢A
32 23 28 29 30 31 offval2 ⊢φ→dx∈XAdSx×fx∈X⟼C+fdx∈XCdSx×fx∈X⟼A=x∈X⟼B⁢C+D⁢A
33 20 27 32 3eqtr3d ⊢φ→dx∈XA⁢CdSx=x∈X⟼B⁢C+D⁢A