This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑋 : 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 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ‘ ( 𝑋 ‘ ∅ ) ) )