mzpf

Description: A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014)

		Ref	Expression
	Assertion	mzpf	$⊢ F \in mzPoly (V) \to F : ℤ^{V} ⟶ ℤ$

Step	Hyp	Ref	Expression
1		elfvex	$⊢ F \in mzPoly (V) \to V \in V$
2		mzpval	$⊢ V \in V \to mzPoly (V) = ⋂ mzPolyCld (V)$
3		mzpclall	$⊢ V \in V \to ℤ^{(ℤ^{V})} \in mzPolyCld (V)$
4		intss1	$⊢ ℤ^{(ℤ^{V})} \in mzPolyCld (V) \to ⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})}$
5	3 4	syl	$⊢ V \in V \to ⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})}$
6	2 5	eqsstrd	$⊢ V \in V \to mzPoly (V) \subseteq ℤ^{(ℤ^{V})}$
7	1 6	syl	$⊢ F \in mzPoly (V) \to mzPoly (V) \subseteq ℤ^{(ℤ^{V})}$
8	7	sselda	$⊢ (F \in mzPoly (V) \land F \in mzPoly (V)) \to F \in (ℤ^{(ℤ^{V})})$
9	8	anidms	$⊢ F \in mzPoly (V) \to F \in (ℤ^{(ℤ^{V})})$
10		zex	$⊢ ℤ \in V$
11		ovex	$⊢ ℤ^{V} \in V$
12	10 11	elmap	$⊢ F \in (ℤ^{(ℤ^{V})}) \leftrightarrow F : ℤ^{V} ⟶ ℤ$
13	9 12	sylib	$⊢ F \in mzPoly (V) \to F : ℤ^{V} ⟶ ℤ$

Metamath Proof Explorer