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	⊢ ( ( 𝐴 ∈ ( 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	simprd	⊢ ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝐴 ∘f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) )