Metamath Proof Explorer

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 ⊢ F ∈ mzPoly ⁡ V → F : ℤ V ⟶ ℤ

Proof

Step Hyp Ref Expression
1 elfvex ⊢ F ∈ mzPoly ⁡ V → V ∈ V
2 mzpval ⊢ V ∈ V → mzPoly ⁡ V = ⋂ mzPolyCld ⁡ V
3 mzpclall ⊢ V ∈ V → ℤ ℤ V ∈ mzPolyCld ⁡ V
4 intss1 ⊢ ℤ ℤ V ∈ mzPolyCld ⁡ V → ⋂ mzPolyCld ⁡ V ⊆ ℤ ℤ V
5 3 4 syl ⊢ V ∈ V → ⋂ mzPolyCld ⁡ V ⊆ ℤ ℤ V
6 2 5 eqsstrd ⊢ V ∈ V → mzPoly ⁡ V ⊆ ℤ ℤ V
7 1 6 syl ⊢ F ∈ mzPoly ⁡ V → mzPoly ⁡ V ⊆ ℤ ℤ V
8 7 sselda ⊢ F ∈ mzPoly ⁡ V ∧ F ∈ mzPoly ⁡ V → F ∈ ℤ ℤ V
9 8 anidms ⊢ F ∈ mzPoly ⁡ V → F ∈ ℤ ℤ V
10 zex ⊢ ℤ ∈ V
11 ovex ⊢ ℤ V ∈ V
12 10 11 elmap ⊢ F ∈ ℤ ℤ V ↔ F : ℤ V ⟶ ℤ
13 9 12 sylib ⊢ F ∈ mzPoly ⁡ V → F : ℤ V ⟶ ℤ