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 \in CRing \to I = 2Ideal (R)$

Step	Hyp	Ref	Expression
1		crng2idl.i	$⊢ I = LIdeal (R)$
2		inidm	$⊢ I \cap I = I$
3		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
4	1 3	crngridl	$⊢ R \in CRing \to I = LIdeal ({opp}_{r} (R))$
5	4	ineq2d	$⊢ R \in CRing \to I \cap I = I \cap LIdeal ({opp}_{r} (R))$
6	2 5	eqtr3id	$⊢ R \in CRing \to I = I \cap 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 \cap LIdeal ({opp}_{r} (R))$
10	6 9	eqtr4di	$⊢ R \in CRing \to I = 2Ideal (R)$

Metamath Proof Explorer