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 e. ( mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( F e. ( mzPoly ` V ) -> V e. _V )
2 mzpval 
 |-  ( V e. _V -> ( mzPoly ` V ) = |^| ( mzPolyCld ` V ) )
3 mzpclall 
 |-  ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) )
4 intss1 
 |-  ( ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) -> |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
5 3 4 syl 
 |-  ( V e. _V -> |^| ( mzPolyCld ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
6 2 5 eqsstrd 
 |-  ( V e. _V -> ( mzPoly ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
7 1 6 syl 
 |-  ( F e. ( mzPoly ` V ) -> ( mzPoly ` V ) C_ ( ZZ ^m ( ZZ ^m V ) ) )
8 7 sselda 
 |-  ( ( F e. ( mzPoly ` V ) /\ F e. ( mzPoly ` V ) ) -> F e. ( ZZ ^m ( ZZ ^m V ) ) )
9 8 anidms 
 |-  ( F e. ( mzPoly ` V ) -> F e. ( ZZ ^m ( ZZ ^m V ) ) )
10 zex 
 |-  ZZ e. _V
11 ovex 
 |-  ( ZZ ^m V ) e. _V
12 10 11 elmap 
 |-  ( F e. ( ZZ ^m ( ZZ ^m V ) ) <-> F : ( ZZ ^m V ) --> ZZ )
13 9 12 sylib 
 |-  ( F e. ( mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ )