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	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A B) \in mzPoly (V)$

Step	Hyp	Ref	Expression
1		mzpf	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A) : ℤ^{V} ⟶ ℤ$
2	1	ffnd	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ A) Fn (ℤ^{V})$
3		mzpf	$⊢ (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ B) : ℤ^{V} ⟶ ℤ$
4	3	ffnd	$⊢ (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ B) Fn (ℤ^{V})$
5		ovex	$⊢ ℤ^{V} \in V$
6		ofmpteq	$⊢ (ℤ^{V} \in V \land (x \in (ℤ^{V}) ⟼ A) Fn (ℤ^{V}) \land (x \in (ℤ^{V}) ⟼ B) Fn (ℤ^{V})) \to (x \in (ℤ^{V}) ⟼ A) \times_{f} (x \in (ℤ^{V}) ⟼ B) = (x \in (ℤ^{V}) ⟼ A B)$
7	5 6	mp3an1	$⊢ ((x \in (ℤ^{V}) ⟼ A) Fn (ℤ^{V}) \land (x \in (ℤ^{V}) ⟼ B) Fn (ℤ^{V})) \to (x \in (ℤ^{V}) ⟼ A) \times_{f} (x \in (ℤ^{V}) ⟼ B) = (x \in (ℤ^{V}) ⟼ A B)$
8	2 4 7	syl2an	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A) \times_{f} (x \in (ℤ^{V}) ⟼ B) = (x \in (ℤ^{V}) ⟼ A B)$
9		mzpmul	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A) \times_{f} (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V)$
10	8 9	eqeltrrd	$⊢ ((x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ B) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ A B) \in mzPoly (V)$

Metamath Proof Explorer