coe1fval

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

		Ref	Expression
	Hypothesis	coe1fval.a	$⊢ A = {coe}_{1} (F)$
	Assertion	coe1fval	$⊢ F \in V \to A = (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\}))$

Step	Hyp	Ref	Expression
1		coe1fval.a	$⊢ A = {coe}_{1} (F)$
2		elex	$⊢ F \in V \to F \in V$
3		fveq1	$⊢ f = F \to f (1_{𝑜} \times \{n\}) = F (1_{𝑜} \times \{n\})$
4	3	mpteq2dv	$⊢ f = F \to (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\})) = (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\}))$
5		df-coe1	$⊢ {coe}_{1} = (f \in V ⟼ (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\})))$
6		nn0ex	$⊢ ℕ_{0} \in V$
7	6	mptex	$⊢ (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\})) \in V$
8	4 5 7	fvmpt	$⊢ F \in V \to {coe}_{1} (F) = (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\}))$
9	1 8	eqtrid	$⊢ F \in V \to A = (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\}))$
10	2 9	syl	$⊢ F \in V \to A = (n \in ℕ_{0} ⟼ F (1_{𝑜} \times \{n\}))$

Metamath Proof Explorer