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={\mathrm{coe}}_1\left(F\right)$$
	coe1sfi.b	$$⊢B={\mathrm{Base}}_P$$
	coe1sfi.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1sfi.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	coe1sfi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1sfi.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		coe1sfi.b	$$⊢B={\mathrm{Base}}_P$$
3		coe1sfi.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		coe1sfi.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8		eqid	$$⊢\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)$$
9	5 6 7 8	mapsncnv	$$⊢{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
10	1 2 3 9	coe1fval2	$$⊢F\in B\to A=F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}$$
11		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
13	3 2	ply1bascl2	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
14	3 2	elbasfv	$$⊢F\in B\to R\in \mathrm{V}$$
15	11 12 4 13 14	mplelsfi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
16	5 6 7 8	mapsnf1o2	$$⊢\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
17		f1ocnv	$$⊢\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
18		f1of1	$$⊢{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}\to {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
19	16 17 18	mp2b	$$⊢{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
20	19	a1i	$$⊢F\in B\to {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
21	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
22	21	a1i	$$⊢F\in B\to \underset{\dot{}}{0}\in \mathrm{V}$$
23		id	$$⊢F\in B\to F\in B$$
24	15 20 22 23	fsuppco	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}\right)\right)$$
25	10 24	eqbrtrd	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(A\right)$$