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

Metamath Proof Explorer

Theorem evl1fvf

Description: The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses evl1fvf.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1fvf.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1fvf.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evl1fvf.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1fvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1fvf.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
Assertion evl1fvf ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 evl1fvf.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2 evl1fvf.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 evl1fvf.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 evl1fvf.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 evl1fvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 evl1fvf.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
7 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
8 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
9 5 fvexi ⊢ 𝐵 ∈ V
10 9 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
11 1 2 7 5 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
12 3 8 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
13 4 11 12 3syl ⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
14 13 6 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
15 7 5 8 4 10 14 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )