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

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. } )