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