Theorem fvcoe1

Description: Value of a multivariate coefficient in terms of the coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	2 3 4	mapsnconst	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X=1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}$$
6	5	adantl	$$⊢\left(F\in V\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to X=1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}$$
7	6	fveq2d	$$⊢\left(F\in V\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\left(X\right)=F\left(1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}\right)$$
8		elmapi	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X:1_{𝑜}⟶{\mathbb{N}}_0$$
9		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
10		ffvelrn	$$⊢\left(X:1_{𝑜}⟶{\mathbb{N}}_0\wedge \varnothing \in 1_{𝑜}\right)\to X\left(\varnothing \right)\in {\mathbb{N}}_0$$
11	8 9 10	sylancl	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X\left(\varnothing \right)\in {\mathbb{N}}_0$$
12	1	coe1fv	$$⊢\left(F\in V\wedge X\left(\varnothing \right)\in {\mathbb{N}}_0\right)\to A\left(X\left(\varnothing \right)\right)=F\left(1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}\right)$$
13	11 12	sylan2	$$⊢\left(F\in V\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to A\left(X\left(\varnothing \right)\right)=F\left(1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}\right)$$
14	7 13	eqtr4d	$$⊢\left(F\in V\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\left(X\right)=A\left(X\left(\varnothing \right)\right)$$