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 ⊢ 𝐼 = ( 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 ‘ 𝑅 ) )