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=\mathrm{LIdeal}\left(R\right)$$
Assertion	crng2idl	$$⊢R\in \mathrm{CRing}\to I=\mathrm{2Ideal}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		crng2idl.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
2		inidm	$$⊢I\cap I=I$$
3		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
4	1 3	crngridl	$$⊢R\in \mathrm{CRing}\to I=\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
5	4	ineq2d	$$⊢R\in \mathrm{CRing}\to I\cap I=I\cap \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
6	2 5	eqtr3id	$$⊢R\in \mathrm{CRing}\to I=I\cap \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
7		eqid	$$⊢\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)=\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
8		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
9	1 3 7 8	2idlval	$$⊢\mathrm{2Ideal}\left(R\right)=I\cap \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
10	6 9	eqtr4di	$$⊢R\in \mathrm{CRing}\to I=\mathrm{2Ideal}\left(R\right)$$