# Metamath Proof Explorer

## Theorem fveval1fvcl

Description: The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019)

Ref Expression
Hypotheses fveval1fvcl.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
fveval1fvcl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
fveval1fvcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
fveval1fvcl.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
fveval1fvcl.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
fveval1fvcl.y ${⊢}{\phi }\to {Y}\in {B}$
fveval1fvcl.m ${⊢}{\phi }\to {M}\in {U}$
Assertion fveval1fvcl ${⊢}{\phi }\to {O}\left({M}\right)\left({Y}\right)\in {B}$

### Proof

Step Hyp Ref Expression
1 fveval1fvcl.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
2 fveval1fvcl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 fveval1fvcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 fveval1fvcl.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
5 fveval1fvcl.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
6 fveval1fvcl.y ${⊢}{\phi }\to {Y}\in {B}$
7 fveval1fvcl.m ${⊢}{\phi }\to {M}\in {U}$
8 eqid ${⊢}{R}{↑}_{𝑠}{B}={R}{↑}_{𝑠}{B}$
9 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
10 3 fvexi ${⊢}{B}\in \mathrm{V}$
11 10 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
12 1 2 8 3 evl1rhm ${⊢}{R}\in \mathrm{CRing}\to {O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)$
13 4 9 rhmf ${⊢}{O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
14 5 12 13 3syl ${⊢}{\phi }\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
15 14 7 ffvelrnd ${⊢}{\phi }\to {O}\left({M}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
16 8 3 9 5 11 15 pwselbas ${⊢}{\phi }\to {O}\left({M}\right):{B}⟶{B}$
17 16 6 ffvelrnd ${⊢}{\phi }\to {O}\left({M}\right)\left({Y}\right)\in {B}$