Theorem evls1rgspncl

Description: Closure of the subring polynomial evaluation in a generated ring. Generic version of cnsrplycl . See also evls1fldgencl . (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 ‘ 𝑅 )
	evls1rgspncl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
Assertion	evls1rgspncl	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )

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		evls1rgspncl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
10		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
11	10	oveq2d	⊢ ( 𝑥 = 𝑋 → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
12	11	mpteq2dv	⊢ ( 𝑥 = 𝑋 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) )
13	12	oveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) )
14		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
15		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
17		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
18	4 1 2 14 3 5 6 9 15 16 17	evls1fpws	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) ) ) )
19		ovexd	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ∈ V )
20	13 18 7 19	fvmptd4	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) )
21		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
22	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
23	22	ringabld	⊢ ( 𝜑 → 𝑅 ∈ Abel )
24		nn0ex	⊢ ℕ0 ∈ V
25	24	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
26	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
27	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
28	6 27	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
29	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
30	28 29	unssd	⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑋 } ) ⊆ 𝐵 )
31	8	a1i	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
32		eqidd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
33	22 26 30 31 32	rgspncl	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ 𝑅 ) )
34		subrgsubg	⊢ ( ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubGrp ‘ 𝑅 ) )
35	33 34	syl	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubGrp ‘ 𝑅 ) )
36	33	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ 𝑅 ) )
37	22 26 30 31 32	rgspnssid	⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑆 ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
39	38	unssad	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ⊆ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
40		eqid	⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
41	17 3 2 40	coe1fvalcl	⊢ ( ( 𝐹 ∈ 𝑈 ∧ 𝑖 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
42	9 41	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
43	14 1	ressbas2	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
44	28 43	syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
46	42 45	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ∈ 𝑆 )
47	39 46	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
48		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
49	48	subrgsubm	⊢ ( ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
50	33 49	syl	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
53		ssun2	⊢ { 𝑋 } ⊆ ( 𝑆 ∪ { 𝑋 } )
54		snidg	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ { 𝑋 } )
55	7 54	syl	⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
56	53 55	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∪ { 𝑋 } ) )
57	37 56	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
58	57	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
59	16	submmulgcl	⊢ ( ( ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑖 ∈ ℕ0 ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
60	51 52 58 59	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
61	15 36 47 60	subrgmcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
62	61	fmpttd	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) : ℕ0 ⟶ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
63	14	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
64	6 63	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
65		eqid	⊢ ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) )
66	2 3 65	mptcoe1fsupp	⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐹 ∈ 𝑈 ) → ( 𝑖 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ) finSupp ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
67	64 9 66	syl2anc	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ) finSupp ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
68		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
69	22 68	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
70		subrgsubg	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
71	6 70	syl	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
72		subgsubm	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝑆 ∈ ( SubMnd ‘ 𝑅 ) )
73	21	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
74	71 72 73	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
75	14 1 21	ress0g	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
76	69 74 28 75	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
77	67 76	breqtrrd	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ) finSupp ( 0g ‘ 𝑅 ) )
78	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
79		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
80	1 15 21 78 79	ringlzd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
81	1	subrgss	⊢ ( ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ⊆ 𝐵 )
82	33 81	syl	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ⊆ 𝐵 )
83	82	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ⊆ 𝐵 )
84	83 60	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐵 )
85	77 80 42 84 74	fsuppssov1	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
86	21 23 25 35 62 85	gsumsubgcl	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
87	20 86	eqeltrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )