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={\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$$
	coe1fvalcl.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	coe1fsupp	$$⊢F\in B\to A\in \left\{g\in \left(K^{{\mathbb{N}}_0}\right)|{finSupp}_{\underset{\dot{}}{0}}\left(g\right)\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		coe1fvalcl.k	$$⊢K={\mathrm{Base}}_R$$
6		breq1	$$⊢g=A\to \left({finSupp}_{\underset{\dot{}}{0}}\left(g\right)\leftrightarrow {finSupp}_{\underset{\dot{}}{0}}\left(A\right)\right)$$
7	1 2 3 5	coe1f	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$
8	5	fvexi	$$⊢K\in \mathrm{V}$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10	8 9	pm3.2i	$$⊢\left(K\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)$$
11		elmapg	$$⊢\left(K\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(A\in \left(K^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶K\right)$$
12	10 11	mp1i	$$⊢F\in B\to \left(A\in \left(K^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶K\right)$$
13	7 12	mpbird	$$⊢F\in B\to A\in \left(K^{{\mathbb{N}}_0}\right)$$
14	1 2 3 4	coe1sfi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(A\right)$$
15	6 13 14	elrabd	$$⊢F\in B\to A\in \left\{g\in \left(K^{{\mathbb{N}}_0}\right)|{finSupp}_{\underset{\dot{}}{0}}\left(g\right)\right\}$$