Theorem evls1fvcl

Description: Variant of fveval1fvcl for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	evls1maprhm.q	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
	evls1maprhm.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	evls1maprhm.b	$$⊢B={\mathrm{Base}}_R$$
	evls1maprhm.u	$$⊢U={\mathrm{Base}}_P$$
	evls1maprhm.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evls1maprhm.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	evls1fvcl.1	$$⊢\phi \to Y\in B$$
	evls1fvcl.2	$$⊢\phi \to M\in U$$
Assertion	evls1fvcl	$$⊢\phi \to O\left(M\right)\left(Y\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
2		evls1maprhm.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
3		evls1maprhm.b	$$⊢B={\mathrm{Base}}_R$$
4		evls1maprhm.u	$$⊢U={\mathrm{Base}}_P$$
5		evls1maprhm.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		evls1maprhm.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7		evls1fvcl.1	$$⊢\phi \to Y\in B$$
8		evls1fvcl.2	$$⊢\phi \to M\in U$$
9		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
10		eqid	$$⊢{\mathrm{eval}}_1\left(R\right)={\mathrm{eval}}_1\left(R\right)$$
11	1 3 2 9 4 10 5 6	ressply1evl	$$⊢\phi \to O={{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U$$
12	11	fveq1d	$$⊢\phi \to O\left(M\right)=\left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U\right)\left(M\right)$$
13	8	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_U\right)\left(M\right)={\mathrm{eval}}_1\left(R\right)\left(M\right)$$
14	12 13	eqtrd	$$⊢\phi \to O\left(M\right)={\mathrm{eval}}_1\left(R\right)\left(M\right)$$
15	14	fveq1d	$$⊢\phi \to O\left(M\right)\left(Y\right)={\mathrm{eval}}_1\left(R\right)\left(M\right)\left(Y\right)$$
16		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
17		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
18		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}U={\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}U$$
19	16 9 2 4 6 18	ressply1bas	$$⊢\phi \to U={\mathrm{Base}}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}U\right)}$$
20	18 17	ressbasss	$$⊢{\mathrm{Base}}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}U\right)}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
21	19 20	eqsstrdi	$$⊢\phi \to U\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
22	21 8	sseldd	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
23	10 16 3 17 5 7 22	fveval1fvcl	$$⊢\phi \to {\mathrm{eval}}_1\left(R\right)\left(M\right)\left(Y\right)\in B$$
24	15 23	eqeltrd	$$⊢\phi \to O\left(M\right)\left(Y\right)\in B$$