Metamath Proof Explorer


Theorem mzpadd

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

Ref Expression
Assertion mzpadd ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝐴f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 elfvex ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
2 1 adantr ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝑉 ∈ V )
3 mzpincl ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )
4 2 3 syl ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )
5 mzpcl34 ( ( ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) )
6 5 3expib ( ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) → ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ) )
7 4 6 mpcom ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) )
8 7 simpld ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝐴f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) )