Metamath Proof Explorer

Theorem mzpmulmpt

Description: Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt . (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpmulmpt ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A ⁢ B ∈ mzPoly ⁡ V

Proof

Step Hyp Ref Expression
1 mzpf ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A : ℤ V ⟶ ℤ
2 1 ffnd ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A Fn ℤ V
3 mzpf ⊢ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ B : ℤ V ⟶ ℤ
4 3 ffnd ⊢ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ B Fn ℤ V
5 ovex ⊢ ℤ V ∈ V
6 ofmpteq ⊢ ℤ V ∈ V ∧ x ∈ ℤ V ⟼ A Fn ℤ V ∧ x ∈ ℤ V ⟼ B Fn ℤ V → x ∈ ℤ V ⟼ A × f x ∈ ℤ V ⟼ B = x ∈ ℤ V ⟼ A ⁢ B
7 5 6 mp3an1 ⊢ x ∈ ℤ V ⟼ A Fn ℤ V ∧ x ∈ ℤ V ⟼ B Fn ℤ V → x ∈ ℤ V ⟼ A × f x ∈ ℤ V ⟼ B = x ∈ ℤ V ⟼ A ⁢ B
8 2 4 7 syl2an ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A × f x ∈ ℤ V ⟼ B = x ∈ ℤ V ⟼ A ⁢ B
9 mzpmul ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A × f x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V
10 8 9 eqeltrrd ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A ⁢ B ∈ mzPoly ⁡ V