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	|- O = ( eval1 ` R )
	evl1fvf.p	|- P = ( Poly1 ` R )
	evl1fvf.u	|- U = ( Base ` P )
	evl1fvf.r	|- ( ph -> R e. CRing )
	evl1fvf.b	|- B = ( Base ` R )
	evl1fvf.q	|- ( ph -> Q e. U )
Assertion	evl1fvf	|- ( ph -> ( O ` Q ) : B --> B )

Proof

Step	Hyp	Ref	Expression
1		evl1fvf.o	|- O = ( eval1 ` R )
2		evl1fvf.p	|- P = ( Poly1 ` R )
3		evl1fvf.u	|- U = ( Base ` P )
4		evl1fvf.r	|- ( ph -> R e. CRing )
5		evl1fvf.b	|- B = ( Base ` R )
6		evl1fvf.q	|- ( ph -> Q e. U )
7		eqid	|- ( R ^s B ) = ( R ^s B )
8		eqid	|- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
9	5	fvexi	|- B e. _V
10	9	a1i	|- ( ph -> B e. _V )
11	1 2 7 5	evl1rhm	|- ( R e. CRing -> O e. ( P RingHom ( R ^s B ) ) )
12	3 8	rhmf	|- ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
13	4 11 12	3syl	|- ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
14	13 6	ffvelcdmd	|- ( ph -> ( O ` Q ) e. ( Base ` ( R ^s B ) ) )
15	7 5 8 4 10 14	pwselbas	|- ( ph -> ( O ` Q ) : B --> B )