This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1basf

Description: Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses ply1rcl.p 
|- P = ( Poly1 ` R )
ply1rcl.b 
|- B = ( Base ` P )
ply1basf.k 
|- K = ( Base ` R )
Assertion ply1basf 
|- ( F e. B -> F : ( NN0 ^m 1o ) --> K )

Proof

Step Hyp Ref Expression
1 ply1rcl.p 
 |-  P = ( Poly1 ` R )
2 ply1rcl.b 
 |-  B = ( Base ` P )
3 ply1basf.k 
 |-  K = ( Base ` R )
4 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
5 eqid 
 |-  ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
6 psr1baslem 
 |-  ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin }
7 id 
 |-  ( F e. B -> F e. B )
8 1 2 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
9 7 8 eleqtrdi 
 |-  ( F e. B -> F e. ( Base ` ( 1o mPoly R ) ) )
10 4 3 5 6 9 mplelf 
 |-  ( F e. B -> F : ( NN0 ^m 1o ) --> K )