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 × f B ∈ 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 + f B ∈ mzPoly ⁡ V ∧ A × f B ∈ mzPoly ⁡ V
6 5 3expib ⊢ mzPoly ⁡ V ∈ mzPolyCld ⁡ V → A ∈ mzPoly ⁡ V ∧ B ∈ mzPoly ⁡ V → A + f B ∈ mzPoly ⁡ V ∧ A × f B ∈ mzPoly ⁡ V
7 4 6 mpcom ⊢ A ∈ mzPoly ⁡ V ∧ B ∈ mzPoly ⁡ V → A + f B ∈ mzPoly ⁡ V ∧ A × f B ∈ mzPoly ⁡ V
8 7 simprd ⊢ A ∈ mzPoly ⁡ V ∧ B ∈ mzPoly ⁡ V → A × f B ∈ mzPoly ⁡ V