Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngunsnply1.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	rngunsnply1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	rngunsnply1.q	⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
	rngunsnply1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rngunsnply1.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	rngunsnply1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	rngunsnply1.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
Assertion	rngunsnply1	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ↔ ∃ 𝑝 ∈ 𝑈 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngunsnply1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rngunsnply1.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		rngunsnply1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		rngunsnply1.q	⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
5		rngunsnply1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		rngunsnply1.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		rngunsnply1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		rngunsnply1.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
9	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
11	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
12	6 11	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
13	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
14	12 13	unssd	⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑋 } ) ⊆ 𝐵 )
15	8	a1i	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
16		eqidd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
17		eqid	⊢ ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
18	4 2 1 3 5 6 7 17	evls1maprhm	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( 𝑃 RingHom 𝑅 ) )
19		rnrhmsubrg	⊢ ( ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( 𝑃 RingHom 𝑅 ) → ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( SubRing ‘ 𝑅 ) )
20	18 19	syl	⊢ ( 𝜑 → ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ∈ ( SubRing ‘ 𝑅 ) )
21	4 2 1 3 5 6 7 17	evls1maprnss	⊢ ( 𝜑 → 𝑆 ⊆ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
22		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
23		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
24	22 6 23 2 3	subrgvr1cl	⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ 𝑈 )
25	22 6 23	subrgvr1	⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
26	25	fveq2d	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) = ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
27	26	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ‘ 𝑋 ) )
28		eqid	⊢ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) )
29	4 28 23 1 5 6	evls1var	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( I ↾ 𝐵 ) )
30	29	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ‘ 𝑋 ) = ( ( I ↾ 𝐵 ) ‘ 𝑋 ) )
31		fvresi	⊢ ( 𝑋 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑋 ) = 𝑋 )
32	7 31	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐵 ) ‘ 𝑋 ) = 𝑋 )
33	27 30 32	3eqtrrd	⊢ ( 𝜑 → 𝑋 = ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑝 = ( var1 ‘ 𝑅 ) ) → 𝑋 = ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) )
35		fveq2	⊢ ( 𝑝 = ( var1 ‘ 𝑅 ) → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) )
36	35	fveq1d	⊢ ( 𝑝 = ( var1 ‘ 𝑅 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑝 = ( var1 ‘ 𝑅 ) ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) )
38	34 37	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑝 = ( var1 ‘ 𝑅 ) ) → 𝑋 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
39	17 24 7 38	elrnmptdv	⊢ ( 𝜑 → 𝑋 ∈ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
40	39	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
41	21 40	unssd	⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑋 } ) ⊆ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
42	9 10 14 15 16 20 41	rgspnmin	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ⊆ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
43	42	sseld	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) → 𝑉 ∈ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ) )
44		fvex	⊢ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ∈ V
45	17 44	elrnmpti	⊢ ( 𝑉 ∈ ran ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) ↔ ∃ 𝑝 ∈ 𝑈 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
46	43 45	imbitrdi	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) → ∃ 𝑝 ∈ 𝑈 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
47	5	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑅 ∈ CRing )
48	6	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
49	7	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
50		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
51	1 2 3 4 47 48 49 8 50	evls1rgspncl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
52		eleq1	⊢ ( 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) → ( 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ↔ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ) )
53	51 52	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) → 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ) )
54	53	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝑈 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) → 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ) )
55	46 54	impbid	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ↔ ∃ 𝑝 ∈ 𝑈 𝑉 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )