This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )