Theorem coe1fv

Description: Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypothesis	coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
Assertion	coe1fv	$$⊢\left(F\in V\wedge N\in {\mathbb{N}}_0\right)\to A\left(N\right)=F\left(1_{𝑜}\times \left\{N\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2	1	coe1fval	$$⊢F\in V\to A=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$
3	2	fveq1d	$$⊢F\in V\to A\left(N\right)=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)\left(N\right)$$
4		sneq	$$⊢n=N\to \left\{n\right\}=\left\{N\right\}$$
5	4	xpeq2d	$$⊢n=N\to 1_{𝑜}\times \left\{n\right\}=1_{𝑜}\times \left\{N\right\}$$
6	5	fveq2d	$$⊢n=N\to F\left(1_{𝑜}\times \left\{n\right\}\right)=F\left(1_{𝑜}\times \left\{N\right\}\right)$$
7		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$
8		fvex	$$⊢F\left(1_{𝑜}\times \left\{N\right\}\right)\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢N\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)\left(N\right)=F\left(1_{𝑜}\times \left\{N\right\}\right)$$
10	3 9	sylan9eq	$$⊢\left(F\in V\wedge N\in {\mathbb{N}}_0\right)\to A\left(N\right)=F\left(1_{𝑜}\times \left\{N\right\}\right)$$