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

Proof

Step	Hyp	Ref	Expression
1		rspidlid.1	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
2		rspidlid.2	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
3		ssid	⊢ 𝐼 ⊆ 𝐼
4	1 2	rspssp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ⊆ 𝐼 ) → ( 𝐾 ‘ 𝐼 ) ⊆ 𝐼 )
5	3 4	mp3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐾 ‘ 𝐼 ) ⊆ 𝐼 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	6 2	lidlss	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
8	1 6	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ⊆ ( Base ‘ 𝑅 ) ) → 𝐼 ⊆ ( 𝐾 ‘ 𝐼 ) )
9	7 8	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ⊆ ( 𝐾 ‘ 𝐼 ) )
10	5 9	eqssd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐾 ‘ 𝐼 ) = 𝐼 )