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	11 12 4 13	mplelsfi	\|- ( F e. B -> F finSupp .0. )
15	5 6 7 8	mapsnf1o2	\|- ( x e. ( NN0 ^m 1o ) \|-> ( x ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
16		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 ) )
17		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 ) )
18	15 16 17	mp2b	\|- `' ( x e. ( NN0 ^m 1o ) \|-> ( x ` (/) ) ) : NN0 -1-1-> ( NN0 ^m 1o )
19	18	a1i	\|- ( F e. B -> `' ( x e. ( NN0 ^m 1o ) \|-> ( x ` (/) ) ) : NN0 -1-1-> ( NN0 ^m 1o ) )
20	4	fvexi	\|- .0. e. _V
21	20	a1i	\|- ( F e. B -> .0. e. _V )
22		id	\|- ( F e. B -> F e. B )
23	14 19 21 22	fsuppco	\|- ( F e. B -> ( F o. `' ( x e. ( NN0 ^m 1o ) \|-> ( x ` (/) ) ) ) finSupp .0. )
24	10 23	eqbrtrd	\|- ( F e. B -> A finSupp .0. )

Metamath Proof Explorer

Theorem coe1sfi

Proof