crngridl

Description: In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015)

Step	Hyp	Ref	Expression
1		crng2idl.i	$⊢ I = LIdeal (R)$
2		crngridl.o	$⊢ O = {opp}_{r} (R)$
3		eqidd	$⊢ R \in CRing \to {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	2 4	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
6	5	a1i	$⊢ R \in CRing \to {Base}_{R} = {Base}_{O}$
7		ssv	$⊢ {Base}_{R} \subseteq V$
8	7	a1i	$⊢ R \in CRing \to {Base}_{R} \subseteq V$
9		eqid	$⊢ +_{R} = +_{R}$
10	2 9	oppradd	$⊢ +_{R} = +_{O}$
11	10	oveqi	$⊢ x +_{R} y = x +_{O} y$
12	11	a1i	$⊢ (R \in CRing \land (x \in V \land y \in V)) \to x +_{R} y = x +_{O} y$
13		ovexd	$⊢ (R \in CRing \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \cdot_{R} y \in V$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15		eqid	$⊢ \cdot_{O} = \cdot_{O}$
16	4 14 2 15	crngoppr	$⊢ (R \in CRing \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y = x \cdot_{O} y$
17	16	3expb	$⊢ (R \in CRing \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \cdot_{R} y = x \cdot_{O} y$
18	3 6 8 12 13 17	lidlrsppropd	$⊢ R \in CRing \to (LIdeal (R) = LIdeal (O) \land RSpan (R) = RSpan (O))$
19	18	simpld	$⊢ R \in CRing \to LIdeal (R) = LIdeal (O)$
20	1 19	syl5eq	$⊢ R \in CRing \to I = LIdeal (O)$

Metamath Proof Explorer