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

Metamath Proof Explorer

Theorem coe1fval

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

Ref Expression
Hypothesis coe1fval.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion coe1fval ( 𝐹 ∈ 𝑉 → 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1fval.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
3 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) = ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) )
4 3 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) )
5 df-coe1 ⊢ coe1 = ( 𝑓 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( 𝑓 ‘ ( 1o × { 𝑛 } ) ) ) )
6 nn0ex ⊢ ℕ0 ∈ V
7 6 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) ∈ V
8 4 5 7 fvmpt ⊢ ( 𝐹 ∈ V → ( coe1 ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) )
9 1 8 eqtrid ⊢ ( 𝐹 ∈ V → 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) )
10 2 9 syl ⊢ ( 𝐹 ∈ 𝑉 → 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑛 } ) ) ) )