Theorem 2idllidld

Description: A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypothesis	2idllidld.1	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
Assertion	2idllidld	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		2idllidld.1	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
2		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
3		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
4		eqid	$$⊢\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)=\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
5		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
6	2 3 4 5	2idlval	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{LIdeal}\left(R\right)\cap \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
7	1 6	eleqtrdi	$$⊢\phi \to I\in \left(\mathrm{LIdeal}\left(R\right)\cap \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)\right)$$
8	7	elin1d	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$