Theorem 2idlridld

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

	Ref	Expression
Hypotheses	2idllidld.1	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	2idlridld.o	$$⊢O={opp}_r\left(R\right)$$
Assertion	2idlridld	$$⊢\phi \to I\in \mathrm{LIdeal}\left(O\right)$$

Proof

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