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 A=coe1F
Assertion coe1fval FVA=n0F1𝑜×n

Proof

Step Hyp Ref Expression
1 coe1fval.a A=coe1F
2 elex FVFV
3 fveq1 f=Ff1𝑜×n=F1𝑜×n
4 3 mpteq2dv f=Fn0f1𝑜×n=n0F1𝑜×n
5 df-coe1 coe1=fVn0f1𝑜×n
6 nn0ex 0V
7 6 mptex n0F1𝑜×nV
8 4 5 7 fvmpt FVcoe1F=n0F1𝑜×n
9 1 8 eqtrid FVA=n0F1𝑜×n
10 2 9 syl FVA=n0F1𝑜×n