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	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )