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