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	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 · 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
2	1	ffnd	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) )
3		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
4	3	ffnd	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) )
5		ovex	⊢ ( ℤ ↑m 𝑉 ) ∈ V
6		ofmpteq	⊢ ( ( ( ℤ ↑m 𝑉 ) ∈ V ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f · ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 · 𝐵 ) ) )
7	5 6	mp3an1	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f · ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 · 𝐵 ) ) )
8	2 4 7	syl2an	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f · ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 · 𝐵 ) ) )
9		mzpmul	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f · ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
10	8 9	eqeltrrd	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 · 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )