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	11 12 4 13	mplelsfi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
15	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$$
16		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_{𝑜}}$$
17		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_{𝑜}}$$
18	15 16 17	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_{𝑜}}$$
19	18	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_{𝑜}}$$
20	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
21	20	a1i	$$⊢F\in B\to \underset{\dot{}}{0}\in \mathrm{V}$$
22		id	$$⊢F\in B\to F\in B$$
23	14 19 21 22	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)$$
24	10 23	eqbrtrd	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(A\right)$$