Theorem 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	⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → 𝐹 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
2		mzpval	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) = ∩ ( mzPolyCld ‘ 𝑉 ) )
3		mzpclall	⊢ ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) )
4		intss1	⊢ ( ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
5	3 4	syl	⊢ ( 𝑉 ∈ V → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
6	2 5	eqsstrd	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
7	1 6	syl	⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → ( mzPoly ‘ 𝑉 ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
8	7	sselda	⊢ ( ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝐹 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
9	8	anidms	⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → 𝐹 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
10		zex	⊢ ℤ ∈ V
11		ovex	⊢ ( ℤ ↑m 𝑉 ) ∈ V
12	10 11	elmap	⊢ ( 𝐹 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ 𝐹 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
13	9 12	sylib	⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → 𝐹 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )