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 = ( RSpan ` R )
	rsp2idlid.2	|- U = ( 2Ideal ` R )
Assertion	rsp2idlid	|- ( ( R e. Ring /\ I e. U ) -> ( K ` I ) = I )

Proof

Step	Hyp	Ref	Expression
1		rsp2idlid.1	|- K = ( RSpan ` R )
2		rsp2idlid.2	|- U = ( 2Ideal ` R )
3	2	eleq2i	|- ( I e. U <-> I e. ( 2Ideal ` R ) )
4	3	biimpi	|- ( I e. U -> I e. ( 2Ideal ` R ) )
5	4	2idllidld	|- ( I e. U -> I e. ( LIdeal ` R ) )
6		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
7	1 6	rspidlid	|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> ( K ` I ) = I )
8	5 7	sylan2	|- ( ( R e. Ring /\ I e. U ) -> ( K ` I ) = I )