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	$⊢ O = R {evalSub}_{1} S$
	evls1maprhm.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
	evls1maprhm.b	$⊢ B = {Base}_{R}$
	evls1maprhm.u	$⊢ U = {Base}_{P}$
	evls1maprhm.r	$⊢ φ \to R \in CRing$
	evls1maprhm.s	$⊢ φ \to S \in SubRing (R)$
	evls1maprhm.y	$⊢ φ \to X \in B$
	evls1maprhm.f	$⊢ F = (p \in U ⟼ O (p) (X))$
Assertion	evls1maprnss	$⊢ φ \to S \subseteq ran F$

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	$⊢ O = R {evalSub}_{1} S$
2		evls1maprhm.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		evls1maprhm.b	$⊢ B = {Base}_{R}$
4		evls1maprhm.u	$⊢ U = {Base}_{P}$
5		evls1maprhm.r	$⊢ φ \to R \in CRing$
6		evls1maprhm.s	$⊢ φ \to S \in SubRing (R)$
7		evls1maprhm.y	$⊢ φ \to X \in B$
8		evls1maprhm.f	$⊢ F = (p \in U ⟼ O (p) (X))$
9		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
10		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
11		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
12		eqid	$⊢ algSc (P) = algSc (P)$
13	9 10 11 2 6 12	subrg1ascl	$⊢ φ \to algSc (P) = {algSc ({Poly}_{1} (R)) ↾}_{S}$
14	13	adantr	$⊢ (φ \land y \in S) \to algSc (P) = {algSc ({Poly}_{1} (R)) ↾}_{S}$
15	14	fveq1d	$⊢ (φ \land y \in S) \to algSc (P) (y) = ({algSc ({Poly}_{1} (R)) ↾}_{S}) (y)$
16		simpr	$⊢ (φ \land y \in S) \to y \in S$
17	16	fvresd	$⊢ (φ \land y \in S) \to ({algSc ({Poly}_{1} (R)) ↾}_{S}) (y) = algSc ({Poly}_{1} (R)) (y)$
18	15 17	eqtrd	$⊢ (φ \land y \in S) \to algSc (P) (y) = algSc ({Poly}_{1} (R)) (y)$
19	6	adantr	$⊢ (φ \land y \in S) \to S \in SubRing (R)$
20	10 11 9 2 4 19 16	asclply1subcl	$⊢ (φ \land y \in S) \to algSc ({Poly}_{1} (R)) (y) \in U$
21	18 20	eqeltrd	$⊢ (φ \land y \in S) \to algSc (P) (y) \in U$
22		fveq2	$⊢ p = algSc (P) (y) \to O (p) = O (algSc (P) (y))$
23	22	fveq1d	$⊢ p = algSc (P) (y) \to O (p) (X) = O (algSc (P) (y)) (X)$
24	23	eqeq2d	$⊢ p = algSc (P) (y) \to (y = O (p) (X) \leftrightarrow y = O (algSc (P) (y)) (X))$
25	24	adantl	$⊢ ((φ \land y \in S) \land p = algSc (P) (y)) \to (y = O (p) (X) \leftrightarrow y = O (algSc (P) (y)) (X))$
26	5	adantr	$⊢ (φ \land y \in S) \to R \in CRing$
27	1 2 11 3 12 26 19 16	evls1sca	$⊢ (φ \land y \in S) \to O (algSc (P) (y)) = B \times \{y\}$
28	27	fveq1d	$⊢ (φ \land y \in S) \to O (algSc (P) (y)) (X) = (B \times \{y\}) (X)$
29	7	adantr	$⊢ (φ \land y \in S) \to X \in B$
30		vex	$⊢ y \in V$
31	30	fvconst2	$⊢ X \in B \to (B \times \{y\}) (X) = y$
32	29 31	syl	$⊢ (φ \land y \in S) \to (B \times \{y\}) (X) = y$
33	28 32	eqtr2d	$⊢ (φ \land y \in S) \to y = O (algSc (P) (y)) (X)$
34	21 25 33	rspcedvd	$⊢ (φ \land y \in S) \to \exists p \in U y = O (p) (X)$
35	8 34 16	elrnmptd	$⊢ (φ \land y \in S) \to y \in ran F$
36	35	ex	$⊢ φ \to (y \in S \to y \in ran F)$
37	36	ssrdv	$⊢ φ \to S \subseteq ran F$

Metamath Proof Explorer

Theorem evls1maprnss

Proof