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 𝐼 = ( LIdeal ‘ 𝑅 )
Assertion crng2idl ( 𝑅 ∈ CRing → 𝐼 = ( 2Ideal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 crng2idl.i 𝐼 = ( LIdeal ‘ 𝑅 )
2 inidm ( 𝐼𝐼 ) = 𝐼
3 eqid ( oppr𝑅 ) = ( oppr𝑅 )
4 1 3 crngridl ( 𝑅 ∈ CRing → 𝐼 = ( LIdeal ‘ ( oppr𝑅 ) ) )
5 4 ineq2d ( 𝑅 ∈ CRing → ( 𝐼𝐼 ) = ( 𝐼 ∩ ( LIdeal ‘ ( oppr𝑅 ) ) ) )
6 2 5 eqtr3id ( 𝑅 ∈ CRing → 𝐼 = ( 𝐼 ∩ ( LIdeal ‘ ( oppr𝑅 ) ) ) )
7 eqid ( LIdeal ‘ ( oppr𝑅 ) ) = ( LIdeal ‘ ( oppr𝑅 ) )
8 eqid ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
9 1 3 7 8 2idlval ( 2Ideal ‘ 𝑅 ) = ( 𝐼 ∩ ( LIdeal ‘ ( oppr𝑅 ) ) )
10 6 9 eqtr4di ( 𝑅 ∈ CRing → 𝐼 = ( 2Ideal ‘ 𝑅 ) )