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={\mathrm{eval}}_1\left(R\right)$$
	evl1fvf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	evl1fvf.u	$$⊢U={\mathrm{Base}}_P$$
	evl1fvf.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1fvf.b	$$⊢B={\mathrm{Base}}_R$$
	evl1fvf.q	$$⊢\phi \to Q\in U$$
Assertion	evl1fvf	$$⊢\phi \to O\left(Q\right):B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		evl1fvf.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1fvf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		evl1fvf.u	$$⊢U={\mathrm{Base}}_P$$
4		evl1fvf.r	$$⊢\phi \to R\in \mathrm{CRing}$$
5		evl1fvf.b	$$⊢B={\mathrm{Base}}_R$$
6		evl1fvf.q	$$⊢\phi \to Q\in U$$
7		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
9	5	fvexi	$$⊢B\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to B\in \mathrm{V}$$
11	1 2 7 5	evl1rhm	$$⊢R\in \mathrm{CRing}\to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
12	3 8	rhmf	$$⊢O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\to O:U⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
13	4 11 12	3syl	$$⊢\phi \to O:U⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
14	13 6	ffvelcdmd	$$⊢\phi \to O\left(Q\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
15	7 5 8 4 10 14	pwselbas	$$⊢\phi \to O\left(Q\right):B⟶B$$