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	$⊢ 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)$
	evls1rgspncl.f	$⊢ φ \to F \in U$
Assertion	evls1rgspncl	$⊢ φ \to Q (F) (X) \in N (S \cup \{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		evls1rgspncl.f	$⊢ φ \to F \in U$
10		oveq2	$⊢ x = X \to i \cdot_{{mulGrp}_{R}} x = i \cdot_{{mulGrp}_{R}} X$
11	10	oveq2d	$⊢ x = X \to {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} x) = {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X)$
12	11	mpteq2dv	$⊢ x = X \to (i \in ℕ_{0} ⟼ {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} x)) = (i \in ℕ_{0} ⟼ {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X))$
13	12	oveq2d	$⊢ x = X \to \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} x)) = \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X))$
14		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
17		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
18	4 1 2 14 3 5 6 9 15 16 17	evls1fpws	$⊢ φ \to Q (F) = (x \in B ⟼ \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} x)))$
19		ovexd	$⊢ φ \to \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X)) \in V$
20	13 18 7 19	fvmptd4	$⊢ φ \to Q (F) (X) = \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X))$
21		eqid	$⊢ 0_{R} = 0_{R}$
22	5	crngringd	$⊢ φ \to R \in Ring$
23	22	ringabld	$⊢ φ \to R \in Abel$
24		nn0ex	$⊢ ℕ_{0} \in V$
25	24	a1i	$⊢ φ \to ℕ_{0} \in V$
26	1	a1i	$⊢ φ \to B = {Base}_{R}$
27	1	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
28	6 27	syl	$⊢ φ \to S \subseteq B$
29	7	snssd	$⊢ φ \to \{X\} \subseteq B$
30	28 29	unssd	$⊢ φ \to S \cup \{X\} \subseteq B$
31	8	a1i	$⊢ φ \to N = RingSpan (R)$
32		eqidd	$⊢ φ \to N (S \cup \{X\}) = N (S \cup \{X\})$
33	22 26 30 31 32	rgspncl	$⊢ φ \to N (S \cup \{X\}) \in SubRing (R)$
34		subrgsubg	$⊢ N (S \cup \{X\}) \in SubRing (R) \to N (S \cup \{X\}) \in SubGrp (R)$
35	33 34	syl	$⊢ φ \to N (S \cup \{X\}) \in SubGrp (R)$
36	33	adantr	$⊢ (φ \land i \in ℕ_{0}) \to N (S \cup \{X\}) \in SubRing (R)$
37	22 26 30 31 32	rgspnssid	$⊢ φ \to S \cup \{X\} \subseteq N (S \cup \{X\})$
38	37	adantr	$⊢ (φ \land i \in ℕ_{0}) \to S \cup \{X\} \subseteq N (S \cup \{X\})$
39	38	unssad	$⊢ (φ \land i \in ℕ_{0}) \to S \subseteq N (S \cup \{X\})$
40		eqid	$⊢ {Base}_{(R ↾_{𝑠} S)} = {Base}_{(R ↾_{𝑠} S)}$
41	17 3 2 40	coe1fvalcl	$⊢ (F \in U \land i \in ℕ_{0}) \to {coe}_{1} (F) (i) \in {Base}_{(R ↾_{𝑠} S)}$
42	9 41	sylan	$⊢ (φ \land i \in ℕ_{0}) \to {coe}_{1} (F) (i) \in {Base}_{(R ↾_{𝑠} S)}$
43	14 1	ressbas2	$⊢ S \subseteq B \to S = {Base}_{(R ↾_{𝑠} S)}$
44	28 43	syl	$⊢ φ \to S = {Base}_{(R ↾_{𝑠} S)}$
45	44	adantr	$⊢ (φ \land i \in ℕ_{0}) \to S = {Base}_{(R ↾_{𝑠} S)}$
46	42 45	eleqtrrd	$⊢ (φ \land i \in ℕ_{0}) \to {coe}_{1} (F) (i) \in S$
47	39 46	sseldd	$⊢ (φ \land i \in ℕ_{0}) \to {coe}_{1} (F) (i) \in N (S \cup \{X\})$
48		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
49	48	subrgsubm	$⊢ N (S \cup \{X\}) \in SubRing (R) \to N (S \cup \{X\}) \in SubMnd ({mulGrp}_{R})$
50	33 49	syl	$⊢ φ \to N (S \cup \{X\}) \in SubMnd ({mulGrp}_{R})$
51	50	adantr	$⊢ (φ \land i \in ℕ_{0}) \to N (S \cup \{X\}) \in SubMnd ({mulGrp}_{R})$
52		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
53		ssun2	$⊢ \{X\} \subseteq S \cup \{X\}$
54		snidg	$⊢ X \in B \to X \in \{X\}$
55	7 54	syl	$⊢ φ \to X \in \{X\}$
56	53 55	sselid	$⊢ φ \to X \in (S \cup \{X\})$
57	37 56	sseldd	$⊢ φ \to X \in N (S \cup \{X\})$
58	57	adantr	$⊢ (φ \land i \in ℕ_{0}) \to X \in N (S \cup \{X\})$
59	16	submmulgcl	$⊢ (N (S \cup \{X\}) \in SubMnd ({mulGrp}_{R}) \land i \in ℕ_{0} \land X \in N (S \cup \{X\})) \to i \cdot_{{mulGrp}_{R}} X \in N (S \cup \{X\})$
60	51 52 58 59	syl3anc	$⊢ (φ \land i \in ℕ_{0}) \to i \cdot_{{mulGrp}_{R}} X \in N (S \cup \{X\})$
61	15 36 47 60	subrgmcld	$⊢ (φ \land i \in ℕ_{0}) \to {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X) \in N (S \cup \{X\})$
62	61	fmpttd	$⊢ φ \to (i \in ℕ_{0} ⟼ {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X)) : ℕ_{0} ⟶ N (S \cup \{X\})$
63	14	subrgring	$⊢ S \in SubRing (R) \to R ↾_{𝑠} S \in Ring$
64	6 63	syl	$⊢ φ \to R ↾_{𝑠} S \in Ring$
65		eqid	$⊢ 0_{(R ↾_{𝑠} S)} = 0_{(R ↾_{𝑠} S)}$
66	2 3 65	mptcoe1fsupp	$⊢ (R ↾_{𝑠} S \in Ring \land F \in U) \to {finSupp}_{0_{(R ↾_{𝑠} S)}} ((i \in ℕ_{0} ⟼ {coe}_{1} (F) (i)))$
67	64 9 66	syl2anc	$⊢ φ \to {finSupp}_{0_{(R ↾_{𝑠} S)}} ((i \in ℕ_{0} ⟼ {coe}_{1} (F) (i)))$
68		ringmnd	$⊢ R \in Ring \to R \in Mnd$
69	22 68	syl	$⊢ φ \to R \in Mnd$
70		subrgsubg	$⊢ S \in SubRing (R) \to S \in SubGrp (R)$
71	6 70	syl	$⊢ φ \to S \in SubGrp (R)$
72		subgsubm	$⊢ S \in SubGrp (R) \to S \in SubMnd (R)$
73	21	subm0cl	$⊢ S \in SubMnd (R) \to 0_{R} \in S$
74	71 72 73	3syl	$⊢ φ \to 0_{R} \in S$
75	14 1 21	ress0g	$⊢ (R \in Mnd \land 0_{R} \in S \land S \subseteq B) \to 0_{R} = 0_{(R ↾_{𝑠} S)}$
76	69 74 28 75	syl3anc	$⊢ φ \to 0_{R} = 0_{(R ↾_{𝑠} S)}$
77	67 76	breqtrrd	$⊢ φ \to {finSupp}_{0_{R}} ((i \in ℕ_{0} ⟼ {coe}_{1} (F) (i)))$
78	22	adantr	$⊢ (φ \land x \in B) \to R \in Ring$
79		simpr	$⊢ (φ \land x \in B) \to x \in B$
80	1 15 21 78 79	ringlzd	$⊢ (φ \land x \in B) \to 0_{R} \cdot_{R} x = 0_{R}$
81	1	subrgss	$⊢ N (S \cup \{X\}) \in SubRing (R) \to N (S \cup \{X\}) \subseteq B$
82	33 81	syl	$⊢ φ \to N (S \cup \{X\}) \subseteq B$
83	82	adantr	$⊢ (φ \land i \in ℕ_{0}) \to N (S \cup \{X\}) \subseteq B$
84	83 60	sseldd	$⊢ (φ \land i \in ℕ_{0}) \to i \cdot_{{mulGrp}_{R}} X \in B$
85	77 80 42 84 74	fsuppssov1	$⊢ φ \to {finSupp}_{0_{R}} ((i \in ℕ_{0} ⟼ {coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X)))$
86	21 23 25 35 62 85	gsumsubgcl	$⊢ φ \to \underset{i \in ℕ_{0}}{\sum_{R}} ({coe}_{1} (F) (i) \cdot_{R} (i \cdot_{{mulGrp}_{R}} X)) \in N (S \cup \{X\})$
87	20 86	eqeltrd	$⊢ φ \to Q (F) (X) \in N (S \cup \{X\})$

Metamath Proof Explorer

Theorem evls1rgspncl

Proof