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	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion	fvcoe1	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ‘ ( 𝑋 ‘ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2		df1o2	⊢ 1o = { ∅ }
3		nn0ex	⊢ ℕ0 ∈ V
4		0ex	⊢ ∅ ∈ V
5	2 3 4	mapsnconst	⊢ ( 𝑋 ∈ ( ℕ0 ↑m 1o ) → 𝑋 = ( 1o × { ( 𝑋 ‘ ∅ ) } ) )
6	5	adantl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 = ( 1o × { ( 𝑋 ‘ ∅ ) } ) )
7	6	fveq2d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ ( 1o × { ( 𝑋 ‘ ∅ ) } ) ) )
8		elmapi	⊢ ( 𝑋 ∈ ( ℕ0 ↑m 1o ) → 𝑋 : 1o ⟶ ℕ0 )
9		0lt1o	⊢ ∅ ∈ 1o
10		ffvelrn	⊢ ( ( 𝑋 : 1o ⟶ ℕ0 ∧ ∅ ∈ 1o ) → ( 𝑋 ‘ ∅ ) ∈ ℕ0 )
11	8 9 10	sylancl	⊢ ( 𝑋 ∈ ( ℕ0 ↑m 1o ) → ( 𝑋 ‘ ∅ ) ∈ ℕ0 )
12	1	coe1fv	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑋 ‘ ∅ ) ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑋 ‘ ∅ ) ) = ( 𝐹 ‘ ( 1o × { ( 𝑋 ‘ ∅ ) } ) ) )
13	11 12	sylan2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐴 ‘ ( 𝑋 ‘ ∅ ) ) = ( 𝐹 ‘ ( 1o × { ( 𝑋 ‘ ∅ ) } ) ) )
14	7 13	eqtr4d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ‘ ( 𝑋 ‘ ∅ ) ) )