Metamath Proof Explorer

Theorem fply1

Description: Conditions for a function to be an univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023)

Ref Expression
Hypotheses fply1.1 
|- .0. = ( 0g ` R )
fply1.2 
|- B = ( Base ` R )
fply1.3 
|- P = ( Base ` ( Poly1 ` R ) )
fply1.4 
|- ( ph -> F : ( NN0 ^m 1o ) --> B )
fply1.5 
|- ( ph -> F finSupp .0. )
Assertion fply1 
|- ( ph -> F e. P )

Proof

Step Hyp Ref Expression
1 fply1.1 
 |-  .0. = ( 0g ` R )
2 fply1.2 
 |-  B = ( Base ` R )
3 fply1.3 
 |-  P = ( Base ` ( Poly1 ` R ) )
4 fply1.4 
 |-  ( ph -> F : ( NN0 ^m 1o ) --> B )
5 fply1.5 
 |-  ( ph -> F finSupp .0. )
6 2 fvexi 
 |-  B e. _V
7 ovex 
 |-  ( NN0 ^m 1o ) e. _V
8 6 7 elmap 
 |-  ( F e. ( B ^m ( NN0 ^m 1o ) ) <-> F : ( NN0 ^m 1o ) --> B )
9 4 8 sylibr 
 |-  ( ph -> F e. ( B ^m ( NN0 ^m 1o ) ) )
10 df1o2 
 |-  1o = { (/) }
11 snfi 
 |-  { (/) } e. Fin
12 10 11 eqeltri 
 |-  1o e. Fin
13 12 a1i 
 |-  ( f e. ( NN0 ^m 1o ) -> 1o e. Fin )
14 elmapi 
 |-  ( f e. ( NN0 ^m 1o ) -> f : 1o --> NN0 )
15 13 14 fisuppfi 
 |-  ( f e. ( NN0 ^m 1o ) -> ( `' f " NN ) e. Fin )
16 15 rabeqc 
 |-  { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } = ( NN0 ^m 1o )
17 16 oveq2i 
 |-  ( B ^m { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } ) = ( B ^m ( NN0 ^m 1o ) )
18 9 17 eleqtrrdi 
 |-  ( ph -> F e. ( B ^m { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } ) )
19 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
20 eqid 
 |-  { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin }
21 eqid 
 |-  ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
22 1oex 
 |-  1o e. _V
23 22 a1i 
 |-  ( ph -> 1o e. _V )
24 19 2 20 21 23 psrbas 
 |-  ( ph -> ( Base ` ( 1o mPwSer R ) ) = ( B ^m { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin } ) )
25 18 24 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( 1o mPwSer R ) ) )
26 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
27 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
28 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
29 27 28 3 ply1bas 
 |-  P = ( Base ` ( 1o mPoly R ) )
30 26 19 21 1 29 mplelbas 
 |-  ( F e. P <-> ( F e. ( Base ` ( 1o mPwSer R ) ) /\ F finSupp .0. ) )
31 25 5 30 sylanbrc 
 |-  ( ph -> F e. P )