# 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 𝑂 = ( eval1𝑅 )
fveval1fvcl.p 𝑃 = ( Poly1𝑅 )
fveval1fvcl.b 𝐵 = ( Base ‘ 𝑅 )
fveval1fvcl.u 𝑈 = ( Base ‘ 𝑃 )
fveval1fvcl.r ( 𝜑𝑅 ∈ CRing )
fveval1fvcl.y ( 𝜑𝑌𝐵 )
fveval1fvcl.m ( 𝜑𝑀𝑈 )
Assertion fveval1fvcl ( 𝜑 → ( ( 𝑂𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )

### Proof

Step Hyp Ref Expression
1 fveval1fvcl.q 𝑂 = ( eval1𝑅 )
2 fveval1fvcl.p 𝑃 = ( Poly1𝑅 )
3 fveval1fvcl.b 𝐵 = ( Base ‘ 𝑅 )
4 fveval1fvcl.u 𝑈 = ( Base ‘ 𝑃 )
5 fveval1fvcl.r ( 𝜑𝑅 ∈ CRing )
6 fveval1fvcl.y ( 𝜑𝑌𝐵 )
7 fveval1fvcl.m ( 𝜑𝑀𝑈 )
8 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
9 eqid ( Base ‘ ( 𝑅s 𝐵 ) ) = ( Base ‘ ( 𝑅s 𝐵 ) )
10 3 fvexi 𝐵 ∈ V
11 10 a1i ( 𝜑𝐵 ∈ V )
12 1 2 8 3 evl1rhm ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) )
13 4 9 rhmf ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) )
14 5 12 13 3syl ( 𝜑𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) )
15 14 7 ffvelrnd ( 𝜑 → ( 𝑂𝑀 ) ∈ ( Base ‘ ( 𝑅s 𝐵 ) ) )
16 8 3 9 5 11 15 pwselbas ( 𝜑 → ( 𝑂𝑀 ) : 𝐵𝐵 )
17 16 6 ffvelrnd ( 𝜑 → ( ( 𝑂𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )