Theorem coe1ae0

Description: The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019)

	Ref	Expression
Hypotheses	coe1ae0.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
	coe1ae0.b	$$⊢B={\mathrm{Base}}_P$$
	coe1ae0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1ae0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	coe1ae0	$$⊢F\in B\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1ae0.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		coe1ae0.b	$$⊢B={\mathrm{Base}}_P$$
3		coe1ae0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		coe1ae0.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	1 2 3 4 5	coe1fsupp	$$⊢F\in B\to A\in \left\{a\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}$$
7		breq1	$$⊢a=A\to \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\leftrightarrow {finSupp}_{\underset{\dot{}}{0}}\left(A\right)\right)$$
8	7	elrab	$$⊢A\in \left\{a\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}\leftrightarrow \left(A\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(A\right)\right)$$
9	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	9	a1i	$$⊢F\in B\to \underset{\dot{}}{0}\in \mathrm{V}$$
11		fsuppmapnn0ub	$$⊢\left(A\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(A\right)\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)\right)$$
12	10 11	sylan2	$$⊢\left(A\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)\wedge F\in B\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(A\right)\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)\right)$$
13	12	impancom	$$⊢\left(A\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(A\right)\right)\to \left(F\in B\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)\right)$$
14	8 13	sylbi	$$⊢A\in \left\{a\in \left({{\mathrm{Base}}_R}^{{\mathbb{N}}_0}\right)|{finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right\}\to \left(F\in B\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)\right)$$
15	6 14	mpcom	$$⊢F\in B\to \exists s\in {\mathbb{N}}_0\forall n\in {\mathbb{N}}_0\left(s<n\to A\left(n\right)=\underset{\dot{}}{0}\right)$$