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