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 = {coe}_{1} (F)$
	Assertion	coe1fv	$⊢ (F \in V \land N \in ℕ_{0}) \to A (N) = F (1_{𝑜} \times \{N\})$

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

Metamath Proof Explorer