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	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	rsp2idlid.2	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
Assertion	rsp2idlid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐾 ‘ 𝐼 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		rsp2idlid.1	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
2		rsp2idlid.2	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
3	2	eleq2i	⊢ ( 𝐼 ∈ 𝑈 ↔ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
4	3	biimpi	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
5	4	2idllidld	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
6		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7	1 6	rspidlid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐾 ‘ 𝐼 ) = 𝐼 )
8	5 7	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐾 ‘ 𝐼 ) = 𝐼 )