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 ) )