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 CRing I = 2Ideal R

Proof

Step Hyp Ref Expression
1 crng2idl.i I = LIdeal R
2 inidm I I = I
3 eqid opp r R = opp r R
4 1 3 crngridl R CRing I = LIdeal opp r R
5 4 ineq2d R CRing I I = I LIdeal opp r R
6 2 5 eqtr3id R CRing I = I LIdeal opp r R
7 eqid LIdeal opp r R = LIdeal opp r R
8 eqid 2Ideal R = 2Ideal R
9 1 3 7 8 2idlval 2Ideal R = I LIdeal opp r R
10 6 9 eqtr4di R CRing I = 2Ideal R