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

Step	Hyp	Ref	Expression
1		coe1fval.a	$⊢ A = {coe}_{1} (F)$
2		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
3		nn0ex	$⊢ ℕ_{0} \in V$
4		0ex	$⊢ \emptyset \in V$
5	2 3 4	mapsnconst	$⊢ X \in ({ℕ_{0}}^{1_{𝑜}}) \to X = 1_{𝑜} \times \{X (\emptyset)\}$
6	5	adantl	$⊢ (F \in V \land X \in ({ℕ_{0}}^{1_{𝑜}})) \to X = 1_{𝑜} \times \{X (\emptyset)\}$
7	6	fveq2d	$⊢ (F \in V \land X \in ({ℕ_{0}}^{1_{𝑜}})) \to F (X) = F (1_{𝑜} \times \{X (\emptyset)\})$
8		elmapi	$⊢ X \in ({ℕ_{0}}^{1_{𝑜}}) \to X : 1_{𝑜} ⟶ ℕ_{0}$
9		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
10		ffvelcdm	$⊢ (X : 1_{𝑜} ⟶ ℕ_{0} \land \emptyset \in 1_{𝑜}) \to X (\emptyset) \in ℕ_{0}$
11	8 9 10	sylancl	$⊢ X \in ({ℕ_{0}}^{1_{𝑜}}) \to X (\emptyset) \in ℕ_{0}$
12	1	coe1fv	$⊢ (F \in V \land X (\emptyset) \in ℕ_{0}) \to A (X (\emptyset)) = F (1_{𝑜} \times \{X (\emptyset)\})$
13	11 12	sylan2	$⊢ (F \in V \land X \in ({ℕ_{0}}^{1_{𝑜}})) \to A (X (\emptyset)) = F (1_{𝑜} \times \{X (\emptyset)\})$
14	7 13	eqtr4d	$⊢ (F \in V \land X \in ({ℕ_{0}}^{1_{𝑜}})) \to F (X) = A (X (\emptyset))$

Metamath Proof Explorer