Theorem rsp2idlid

Description: The ideal span of a two-sided ideal is the ideal itself. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 24-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		rsp2idlid.1	$$⊢K=\mathrm{RSpan}\left(R\right)$$
2		rsp2idlid.2	$$⊢U=\mathrm{2Ideal}\left(R\right)$$
3	2	eleq2i	$$⊢I\in U\leftrightarrow I\in \mathrm{2Ideal}\left(R\right)$$
4	3	biimpi	$$⊢I\in U\to I\in \mathrm{2Ideal}\left(R\right)$$
5	4	2idllidld	$$⊢I\in U\to I\in \mathrm{LIdeal}\left(R\right)$$
6		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
7	1 6	rspidlid	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to K\left(I\right)=I$$
8	5 7	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to K\left(I\right)=I$$