Theorem rspidlid

Description: The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	rspidlid.1	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	rspidlid.2	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
Assertion	rspidlid	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to K\left(I\right)=I$$

Proof

Step	Hyp	Ref	Expression
1		rspidlid.1	$$⊢K=\mathrm{RSpan}\left(R\right)$$
2		rspidlid.2	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
3		ssid	$$⊢I\subseteq I$$
4	1 2	rspssp	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\wedge I\subseteq I\right)\to K\left(I\right)\subseteq I$$
5	3 4	mp3an3	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to K\left(I\right)\subseteq I$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7	6 2	lidlss	$$⊢I\in U\to I\subseteq {\mathrm{Base}}_R$$
8	1 6	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge I\subseteq {\mathrm{Base}}_R\right)\to I\subseteq K\left(I\right)$$
9	7 8	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to I\subseteq K\left(I\right)$$
10	5 9	eqssd	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to K\left(I\right)=I$$