Theorem rspvalint

Description: The ideal generated by a subset of a ring as intersection of ideals including the subset. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

	Ref	Expression
Hypotheses	rspvalint.v	$$⊢B={\mathrm{Base}}_R$$
	rspvalint.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	rspvalint.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
Assertion	rspvalint	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to K\left(S\right)=\bigcap \left\{t\in I|S\subseteq t\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rspvalint.v	$$⊢B={\mathrm{Base}}_R$$
2		rspvalint.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
3		rspvalint.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
4		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
5	3 4	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
6	5	fveq1i	$$⊢K\left(S\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)\left(S\right)$$
7	6	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to K\left(S\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)\left(S\right)$$
8		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
9		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
10	1 9	eqtri	$$⊢B={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
11	10	sseq2i	$$⊢S\subseteq B\leftrightarrow S\subseteq {\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
12	11	bilani	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to S\subseteq {\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
14		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
15		eqid	$$⊢\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
16	13 14 15	lspval	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge S\subseteq {\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}\right)\to \mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)\left(S\right)=\bigcap \left\{t\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)|S\subseteq t\right\}$$
17	8 12 16	syl2an2r	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to \mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)\left(S\right)=\bigcap \left\{t\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)|S\subseteq t\right\}$$
18		lidlval	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
19	2 18	eqtr2i	$$⊢\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)=I$$
20	19	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)=I$$
21	20	rabeqdv	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to \left\{t\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)|S\subseteq t\right\}=\left\{t\in I|S\subseteq t\right\}$$
22	21	inteqd	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to \bigcap \left\{t\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)|S\subseteq t\right\}=\bigcap \left\{t\in I|S\subseteq t\right\}$$
23	7 17 22	3eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge S\subseteq B\right)\to K\left(S\right)=\bigcap \left\{t\in I|S\subseteq t\right\}$$