Theorem coe1sfi

Description: Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 19-Jul-2019)

	Ref	Expression
Hypotheses	coe1sfi.a	|- A = ( coe1 ` F )
	coe1sfi.b	|- B = ( Base ` P )
	coe1sfi.p	|- P = ( Poly1 ` R )
	coe1sfi.z	|- .0. = ( 0g ` R )
Assertion	coe1sfi	|- ( F e. B -> A 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		df1o2	|- 1o = { (/) }
6		nn0ex	|- NN0 e. _V
7		0ex	|- (/) e. _V
8		eqid	|- ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) = ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) )
9	5 6 7 8	mapsncnv	|- `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) = ( y e. NN0 |-> ( 1o X. { y } ) )
10	1 2 3 9	coe1fval2	|- ( F e. B -> A = ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) )
11		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
12		eqid	|- ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
13	3 2	ply1bascl2	|- ( F e. B -> F e. ( Base ` ( 1o mPoly R ) ) )
14	3 2	elbasfv	|- ( F e. B -> R e. _V )
15	11 12 4 13 14	mplelsfi	|- ( F e. B -> F finSupp .0. )
16	5 6 7 8	mapsnf1o2	|- ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
17		f1ocnv	|- ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) )
18		f1of1	|- ( `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) -> `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : NN0 -1-1-> ( NN0 ^m 1o ) )
19	16 17 18	mp2b	|- `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : NN0 -1-1-> ( NN0 ^m 1o )
20	19	a1i	|- ( F e. B -> `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) : NN0 -1-1-> ( NN0 ^m 1o ) )
21	4	fvexi	|- .0. e. _V
22	21	a1i	|- ( F e. B -> .0. e. _V )
23		id	|- ( F e. B -> F e. B )
24	15 20 22 23	fsuppco	|- ( F e. B -> ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) finSupp .0. )
25	10 24	eqbrtrd	|- ( F e. B -> A finSupp .0. )