rngunsnply1

Description: Adjoining one element to a ring results in a set of polynomial evaluations. Generalization of rngunsnply . (Contributed by Thierry Arnoux, 8-Nov-2026)

	Ref	Expression
Hypotheses	rngunsnply1.b	$⊢ B = {Base}_{R}$
	rngunsnply1.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
	rngunsnply1.u	$⊢ U = {Base}_{P}$
	rngunsnply1.q	$⊢ Q = R {evalSub}_{1} S$
	rngunsnply1.r	$⊢ φ \to R \in CRing$
	rngunsnply1.s	$⊢ φ \to S \in SubRing (R)$
	rngunsnply1.x	$⊢ φ \to X \in B$
	rngunsnply1.n	$⊢ N = RingSpan (R)$
Assertion	rngunsnply1	$⊢ φ \to (V \in N (S \cup \{X\}) \leftrightarrow \exists p \in U V = Q (p) (X))$

Proof

Step	Hyp	Ref	Expression
1		rngunsnply1.b	$⊢ B = {Base}_{R}$
2		rngunsnply1.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		rngunsnply1.u	$⊢ U = {Base}_{P}$
4		rngunsnply1.q	$⊢ Q = R {evalSub}_{1} S$
5		rngunsnply1.r	$⊢ φ \to R \in CRing$
6		rngunsnply1.s	$⊢ φ \to S \in SubRing (R)$
7		rngunsnply1.x	$⊢ φ \to X \in B$
8		rngunsnply1.n	$⊢ N = RingSpan (R)$
9	5	crngringd	$⊢ φ \to R \in Ring$
10	1	a1i	$⊢ φ \to B = {Base}_{R}$
11	1	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
12	6 11	syl	$⊢ φ \to S \subseteq B$
13	7	snssd	$⊢ φ \to \{X\} \subseteq B$
14	12 13	unssd	$⊢ φ \to S \cup \{X\} \subseteq B$
15	8	a1i	$⊢ φ \to N = RingSpan (R)$
16		eqidd	$⊢ φ \to N (S \cup \{X\}) = N (S \cup \{X\})$
17		eqid	$⊢ (p \in U ⟼ Q (p) (X)) = (p \in U ⟼ Q (p) (X))$
18	4 2 1 3 5 6 7 17	evls1maprhm	$⊢ φ \to (p \in U ⟼ Q (p) (X)) \in (P RingHom R)$
19		rnrhmsubrg	$⊢ (p \in U ⟼ Q (p) (X)) \in (P RingHom R) \to ran (p \in U ⟼ Q (p) (X)) \in SubRing (R)$
20	18 19	syl	$⊢ φ \to ran (p \in U ⟼ Q (p) (X)) \in SubRing (R)$
21	4 2 1 3 5 6 7 17	evls1maprnss	$⊢ φ \to S \subseteq ran (p \in U ⟼ Q (p) (X))$
22		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
23		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
24	22 6 23 2 3	subrgvr1cl	$⊢ φ \to {var}_{1} (R) \in U$
25	22 6 23	subrgvr1	$⊢ φ \to {var}_{1} (R) = {var}_{1} (R ↾_{𝑠} S)$
26	25	fveq2d	$⊢ φ \to Q ({var}_{1} (R)) = Q ({var}_{1} (R ↾_{𝑠} S))$
27	26	fveq1d	$⊢ φ \to Q ({var}_{1} (R)) (X) = Q ({var}_{1} (R ↾_{𝑠} S)) (X)$
28		eqid	$⊢ {var}_{1} (R ↾_{𝑠} S) = {var}_{1} (R ↾_{𝑠} S)$
29	4 28 23 1 5 6	evls1var	$⊢ φ \to Q ({var}_{1} (R ↾_{𝑠} S)) = {I ↾}_{B}$
30	29	fveq1d	$⊢ φ \to Q ({var}_{1} (R ↾_{𝑠} S)) (X) = ({I ↾}_{B}) (X)$
31		fvresi	$⊢ X \in B \to ({I ↾}_{B}) (X) = X$
32	7 31	syl	$⊢ φ \to ({I ↾}_{B}) (X) = X$
33	27 30 32	3eqtrrd	$⊢ φ \to X = Q ({var}_{1} (R)) (X)$
34	33	adantr	$⊢ (φ \land p = {var}_{1} (R)) \to X = Q ({var}_{1} (R)) (X)$
35		fveq2	$⊢ p = {var}_{1} (R) \to Q (p) = Q ({var}_{1} (R))$
36	35	fveq1d	$⊢ p = {var}_{1} (R) \to Q (p) (X) = Q ({var}_{1} (R)) (X)$
37	36	adantl	$⊢ (φ \land p = {var}_{1} (R)) \to Q (p) (X) = Q ({var}_{1} (R)) (X)$
38	34 37	eqtr4d	$⊢ (φ \land p = {var}_{1} (R)) \to X = Q (p) (X)$
39	17 24 7 38	elrnmptdv	$⊢ φ \to X \in ran (p \in U ⟼ Q (p) (X))$
40	39	snssd	$⊢ φ \to \{X\} \subseteq ran (p \in U ⟼ Q (p) (X))$
41	21 40	unssd	$⊢ φ \to S \cup \{X\} \subseteq ran (p \in U ⟼ Q (p) (X))$
42	9 10 14 15 16 20 41	rgspnmin	$⊢ φ \to N (S \cup \{X\}) \subseteq ran (p \in U ⟼ Q (p) (X))$
43	42	sseld	$⊢ φ \to (V \in N (S \cup \{X\}) \to V \in ran (p \in U ⟼ Q (p) (X)))$
44		fvex	$⊢ Q (p) (X) \in V$
45	17 44	elrnmpti	$⊢ V \in ran (p \in U ⟼ Q (p) (X)) \leftrightarrow \exists p \in U V = Q (p) (X)$
46	43 45	imbitrdi	$⊢ φ \to (V \in N (S \cup \{X\}) \to \exists p \in U V = Q (p) (X))$
47	5	adantr	$⊢ (φ \land p \in U) \to R \in CRing$
48	6	adantr	$⊢ (φ \land p \in U) \to S \in SubRing (R)$
49	7	adantr	$⊢ (φ \land p \in U) \to X \in B$
50		simpr	$⊢ (φ \land p \in U) \to p \in U$
51	1 2 3 4 47 48 49 8 50	evls1rgspncl	$⊢ (φ \land p \in U) \to Q (p) (X) \in N (S \cup \{X\})$
52		eleq1	$⊢ V = Q (p) (X) \to (V \in N (S \cup \{X\}) \leftrightarrow Q (p) (X) \in N (S \cup \{X\}))$
53	51 52	syl5ibrcom	$⊢ (φ \land p \in U) \to (V = Q (p) (X) \to V \in N (S \cup \{X\}))$
54	53	rexlimdva	$⊢ φ \to (\exists p \in U V = Q (p) (X) \to V \in N (S \cup \{X\}))$
55	46 54	impbid	$⊢ φ \to (V \in N (S \cup \{X\}) \leftrightarrow \exists p \in U V = Q (p) (X))$

Metamath Proof Explorer

Theorem rngunsnply1

Proof