Theorem evls1fvf

Description: The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	evls1fn.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
	evls1fn.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	evls1fn.u	$$⊢U={\mathrm{Base}}_P$$
	evls1fn.1	$$⊢\phi \to R\in \mathrm{CRing}$$
	evls1fn.2	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	evls1fvf.b	$$⊢B={\mathrm{Base}}_R$$
	evls1fvf.q	$$⊢\phi \to Q\in U$$
Assertion	evls1fvf	$$⊢\phi \to O\left(Q\right):B⟶B$$

Proof

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