ressasclcl

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

	Ref	Expression
Hypotheses	ressasclcl.w	\|- W = ( Poly1 ` U )
	ressasclcl.u	\|- U = ( S \|`s R )
	ressasclcl.a	\|- A = ( algSc ` W )
	ressasclcl.1	\|- B = ( Base ` W )
	ressasclcl.s	\|- ( ph -> S e. CRing )
	ressasclcl.r	\|- ( ph -> R e. ( SubRing ` S ) )
	ressasclcl.x	\|- ( ph -> X e. R )
Assertion	ressasclcl	\|- ( ph -> ( A ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		ressasclcl.w	\|- W = ( Poly1 ` U )
2		ressasclcl.u	\|- U = ( S \|`s R )
3		ressasclcl.a	\|- A = ( algSc ` W )
4		ressasclcl.1	\|- B = ( Base ` W )
5		ressasclcl.s	\|- ( ph -> S e. CRing )
6		ressasclcl.r	\|- ( ph -> R e. ( SubRing ` S ) )
7		ressasclcl.x	\|- ( ph -> X e. R )
8		eqid	\|- ( Base ` S ) = ( Base ` S )
9	8	subrgss	\|- ( R e. ( SubRing ` S ) -> R C_ ( Base ` S ) )
10	2 8	ressbas2	\|- ( R C_ ( Base ` S ) -> R = ( Base ` U ) )
11	6 9 10	3syl	\|- ( ph -> R = ( Base ` U ) )
12	2	subrgcrng	\|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
13	5 6 12	syl2anc	\|- ( ph -> U e. CRing )
14	1	ply1sca	\|- ( U e. CRing -> U = ( Scalar ` W ) )
15	13 14	syl	\|- ( ph -> U = ( Scalar ` W ) )
16	15	fveq2d	\|- ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) )
17	11 16	eqtrd	\|- ( ph -> R = ( Base ` ( Scalar ` W ) ) )
18	7 17	eleqtrd	\|- ( ph -> X e. ( Base ` ( Scalar ` W ) ) )
19		eqid	\|- ( Scalar ` W ) = ( Scalar ` W )
20		eqid	\|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
21		eqid	\|- ( .s ` W ) = ( .s ` W )
22		eqid	\|- ( 1r ` W ) = ( 1r ` W )
23	3 19 20 21 22	asclval	\|- ( X e. ( Base ` ( Scalar ` W ) ) -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) )
24	18 23	syl	\|- ( ph -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) )
25	13	crngringd	\|- ( ph -> U e. Ring )
26	1	ply1lmod	\|- ( U e. Ring -> W e. LMod )
27	25 26	syl	\|- ( ph -> W e. LMod )
28	1	ply1ring	\|- ( U e. Ring -> W e. Ring )
29	4 22	ringidcl	\|- ( W e. Ring -> ( 1r ` W ) e. B )
30	25 28 29	3syl	\|- ( ph -> ( 1r ` W ) e. B )
31	4 19 21 20 27 18 30	lmodvscld	\|- ( ph -> ( X ( .s ` W ) ( 1r ` W ) ) e. B )
32	24 31	eqeltrd	\|- ( ph -> ( A ` X ) e. B )

Metamath Proof Explorer

Theorem ressasclcl

Proof