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