Metamath Proof Explorer


Theorem coe1fsupp

Description: The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019)

Ref Expression
Hypotheses coe1sfi.a
|- A = ( coe1 ` F )
coe1sfi.b
|- B = ( Base ` P )
coe1sfi.p
|- P = ( Poly1 ` R )
coe1sfi.z
|- .0. = ( 0g ` R )
coe1fvalcl.k
|- K = ( Base ` R )
Assertion coe1fsupp
|- ( F e. B -> A e. { g e. ( K ^m NN0 ) | g finSupp .0. } )

Proof

Step Hyp Ref Expression
1 coe1sfi.a
 |-  A = ( coe1 ` F )
2 coe1sfi.b
 |-  B = ( Base ` P )
3 coe1sfi.p
 |-  P = ( Poly1 ` R )
4 coe1sfi.z
 |-  .0. = ( 0g ` R )
5 coe1fvalcl.k
 |-  K = ( Base ` R )
6 breq1
 |-  ( g = A -> ( g finSupp .0. <-> A finSupp .0. ) )
7 1 2 3 5 coe1f
 |-  ( F e. B -> A : NN0 --> K )
8 5 fvexi
 |-  K e. _V
9 nn0ex
 |-  NN0 e. _V
10 8 9 pm3.2i
 |-  ( K e. _V /\ NN0 e. _V )
11 elmapg
 |-  ( ( K e. _V /\ NN0 e. _V ) -> ( A e. ( K ^m NN0 ) <-> A : NN0 --> K ) )
12 10 11 mp1i
 |-  ( F e. B -> ( A e. ( K ^m NN0 ) <-> A : NN0 --> K ) )
13 7 12 mpbird
 |-  ( F e. B -> A e. ( K ^m NN0 ) )
14 1 2 3 4 coe1sfi
 |-  ( F e. B -> A finSupp .0. )
15 6 13 14 elrabd
 |-  ( F e. B -> A e. { g e. ( K ^m NN0 ) | g finSupp .0. } )