Theorem crngridl

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

	Ref	Expression
Hypotheses	crng2idl.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	crngridl.o	$$⊢O={opp}_r\left(R\right)$$
Assertion	crngridl	$$⊢R\in \mathrm{CRing}\to I=\mathrm{LIdeal}\left(O\right)$$

Proof

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