Theorem evls1maprnss

Description: The function F mapping polynomials p to their subring evaluation at a given point A takes all values in the subring S . (Contributed by Thierry Arnoux, 25-Feb-2025)

	Ref	Expression
Hypotheses	evls1maprhm.q	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	evls1maprhm.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	evls1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evls1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evls1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evls1maprhm.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	evls1maprhm.y	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	evls1maprhm.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
Assertion	evls1maprnss	⊢ ( 𝜑 → 𝑆 ⊆ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		evls1maprhm.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		evls1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evls1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
5		evls1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		evls1maprhm.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		evls1maprhm.y	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		evls1maprhm.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
9		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
10		eqid	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
11		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
12		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13	9 10 11 2 6 12	subrg1ascl	⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( algSc ‘ 𝑃 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) )
15	14	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) = ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝑦 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
17	16	fvresd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) )
18	15 17	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
20	10 11 9 2 4 19 16	asclply1subcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) ∈ 𝑈 )
21	18 20	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ∈ 𝑈 )
22		fveq2	⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) )
23	22	fveq1d	⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) )
24	23	eqeq2d	⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ↔ 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) ) )
25	24	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) → ( 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ↔ 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) ) )
26	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑅 ∈ CRing )
27	1 2 11 3 12 26 19 16	evls1sca	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) = ( 𝐵 × { 𝑦 } ) )
28	27	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) = ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) )
29	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
30		vex	⊢ 𝑦 ∈ V
31	30	fvconst2	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
32	29 31	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
33	28 32	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) )
34	21 25 33	rspcedvd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ∃ 𝑝 ∈ 𝑈 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
35	8 34 16	elrnmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ran 𝐹 )
36	35	ex	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ran 𝐹 ) )
37	36	ssrdv	⊢ ( 𝜑 → 𝑆 ⊆ ran 𝐹 )