Theorem coe1fval

Description: Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		elex	$$⊢F\in V\to F\in \mathrm{V}$$
3		fveq1	$$⊢f=F\to f\left(1_{𝑜}\times \left\{n\right\}\right)=F\left(1_{𝑜}\times \left\{n\right\}\right)$$
4	3	mpteq2dv	$$⊢f=F\to \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)$$
5		df-coe1	$$⊢{\mathrm{coe}}_1=\left(f\in \mathrm{V}⟼\left(n\in {\mathbb{N}}_0⟼f\left(1_{𝑜}\times \left\{n\right\}\right)\right)\right)$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7	6	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)\in \mathrm{V}$$
8	4 5 7	fvmpt	$$⊢F\in \mathrm{V}\to {\mathrm{coe}}_1\left(F\right)=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$
9	1 8	syl5eq	$$⊢F\in \mathrm{V}\to A=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$
10	2 9	syl	$$⊢F\in V\to A=\left(n\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{n\right\}\right)\right)$$