Theorem ressasclcl

Description: Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	ressasclcl.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	ressasclcl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	ressasclcl.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	ressasclcl.1	$$⊢B={\mathrm{Base}}_W$$
	ressasclcl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	ressasclcl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	ressasclcl.x	$$⊢\phi \to X\in R$$
Assertion	ressasclcl	$$⊢\phi \to A\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		ressasclcl.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
2		ressasclcl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
3		ressasclcl.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
4		ressasclcl.1	$$⊢B={\mathrm{Base}}_W$$
5		ressasclcl.s	$$⊢\phi \to S\in \mathrm{CRing}$$
6		ressasclcl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
7		ressasclcl.x	$$⊢\phi \to X\in R$$
8		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
9	8	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq {\mathrm{Base}}_S$$
10	2 8	ressbas2	$$⊢R\subseteq {\mathrm{Base}}_S\to R={\mathrm{Base}}_U$$
11	6 9 10	3syl	$$⊢\phi \to R={\mathrm{Base}}_U$$
12	2	subrgcrng	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to U\in \mathrm{CRing}$$
13	5 6 12	syl2anc	$$⊢\phi \to U\in \mathrm{CRing}$$
14	1	ply1sca	$$⊢U\in \mathrm{CRing}\to U=\mathrm{Scalar}\left(W\right)$$
15	13 14	syl	$$⊢\phi \to U=\mathrm{Scalar}\left(W\right)$$
16	15	fveq2d	$$⊢\phi \to {\mathrm{Base}}_U={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17	11 16	eqtrd	$$⊢\phi \to R={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
18	7 17	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
19		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
20		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
21		eqid	$$⊢{\cdot }_W={\cdot }_W$$
22		eqid	$$⊢1_W=1_W$$
23	3 19 20 21 22	asclval	$$⊢X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\to A\left(X\right)=X{\cdot }_W{1}_W$$
24	18 23	syl	$$⊢\phi \to A\left(X\right)=X{\cdot }_W{1}_W$$
25	13	crngringd	$$⊢\phi \to U\in \mathrm{Ring}$$
26	1	ply1lmod	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
27	25 26	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
28	1	ply1ring	$$⊢U\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
29	4 22	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in B$$
30	25 28 29	3syl	$$⊢\phi \to 1_W\in B$$
31	4 19 21 20 27 18 30	lmodvscld	$$⊢\phi \to X{\cdot }_W{1}_W\in B$$
32	24 31	eqeltrd	$$⊢\phi \to A\left(X\right)\in B$$