Theorem ressasclcl

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

	Ref	Expression
Hypotheses	ressasclcl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	ressasclcl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	ressasclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	ressasclcl.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
	ressasclcl.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	ressasclcl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	ressasclcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion	ressasclcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ressasclcl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
2		ressasclcl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3		ressasclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
4		ressasclcl.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
5		ressasclcl.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
6		ressasclcl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
7		ressasclcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
8		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9	8	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
10	2 8	ressbas2	⊢ ( 𝑅 ⊆ ( Base ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
11	6 9 10	3syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
12	2	subrgcrng	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
13	5 6 12	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ CRing )
14	1	ply1sca	⊢ ( 𝑈 ∈ CRing → 𝑈 = ( Scalar ‘ 𝑊 ) )
15	13 14	syl	⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17	11 16	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18	7 17	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
21		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
22		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
23	3 19 20 21 22	asclval	⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
24	18 23	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
25	13	crngringd	⊢ ( 𝜑 → 𝑈 ∈ Ring )
26	1	ply1lmod	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
27	25 26	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
28	1	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
29	4 22	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
30	25 28 29	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
31	4 19 21 20 27 18 30	lmodvscld	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
32	24 31	eqeltrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )