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

Metamath Proof Explorer

Theorem crng2idl

Description: In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypothesis crng2idl.i 
|- I = ( LIdeal ` R )
Assertion crng2idl 
|- ( R e. CRing -> I = ( 2Ideal ` R ) )

Proof

Step Hyp Ref Expression
1 crng2idl.i 
 |-  I = ( LIdeal ` R )
2 inidm 
 |-  ( I i^i I ) = I
3 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
4 1 3 crngridl 
 |-  ( R e. CRing -> I = ( LIdeal ` ( oppR ` R ) ) )
5 4 ineq2d 
 |-  ( R e. CRing -> ( I i^i I ) = ( I i^i ( LIdeal ` ( oppR ` R ) ) ) )
6 2 5 eqtr3id 
 |-  ( R e. CRing -> I = ( I i^i ( LIdeal ` ( oppR ` R ) ) ) )
7 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
8 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
9 1 3 7 8 2idlval 
 |-  ( 2Ideal ` R ) = ( I i^i ( LIdeal ` ( oppR ` R ) ) )
10 6 9 eqtr4di 
 |-  ( R e. CRing -> I = ( 2Ideal ` R ) )