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

Proof

Step	Hyp	Ref	Expression
1		rspidlid.1	|- K = ( RSpan ` R )
2		rspidlid.2	|- U = ( LIdeal ` R )
3		ssid	|- I C_ I
4	1 2	rspssp	|- ( ( R e. Ring /\ I e. U /\ I C_ I ) -> ( K ` I ) C_ I )
5	3 4	mp3an3	|- ( ( R e. Ring /\ I e. U ) -> ( K ` I ) C_ I )
6		eqid	|- ( Base ` R ) = ( Base ` R )
7	6 2	lidlss	|- ( I e. U -> I C_ ( Base ` R ) )
8	1 6	rspssid	|- ( ( R e. Ring /\ I C_ ( Base ` R ) ) -> I C_ ( K ` I ) )
9	7 8	sylan2	|- ( ( R e. Ring /\ I e. U ) -> I C_ ( K ` I ) )
10	5 9	eqssd	|- ( ( R e. Ring /\ I e. U ) -> ( K ` I ) = I )