Metamath Proof Explorer

Theorem mzpaddmpt

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

Ref Expression
Assertion mzpaddmpt ⊢ 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 mzpadd ⊢ 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