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

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
16 8 3 9 5 11 15 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) : 𝐵 ⟶ 𝐵 )
17 16 6 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )