Metamath Proof Explorer

Theorem mzpmul

Description: The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpmul ⊢A∈mzPoly⁡V∧B∈mzPoly⁡V→A×fB∈mzPoly⁡V

Proof

Step Hyp Ref Expression
1 elfvex ⊢A∈mzPoly⁡V→V∈V
2 1 adantr ⊢A∈mzPoly⁡V∧B∈mzPoly⁡V→V∈V
3 mzpincl ⊢V∈V→mzPoly⁡V∈mzPolyCld⁡V
4 2 3 syl ⊢A∈mzPoly⁡V∧B∈mzPoly⁡V→mzPoly⁡V∈mzPolyCld⁡V
5 mzpcl34 ⊢mzPoly⁡V∈mzPolyCld⁡V∧A∈mzPoly⁡V∧B∈mzPoly⁡V→A+fB∈mzPoly⁡V∧A×fB∈mzPoly⁡V
6 5 3expib ⊢mzPoly⁡V∈mzPolyCld⁡V→A∈mzPoly⁡V∧B∈mzPoly⁡V→A+fB∈mzPoly⁡V∧A×fB∈mzPoly⁡V
7 4 6 mpcom ⊢A∈mzPoly⁡V∧B∈mzPoly⁡V→A+fB∈mzPoly⁡V∧A×fB∈mzPoly⁡V
8 7 simprd ⊢A∈mzPoly⁡V∧B∈mzPoly⁡V→A×fB∈mzPoly⁡V