ressasclcl

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

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

Metamath Proof Explorer