Theorem 2idlelb

Description: Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	2idlel.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	2idlel.o	$$⊢O={opp}_r\left(R\right)$$
	2idlel.j	$$⊢J=\mathrm{LIdeal}\left(O\right)$$
	2idlel.t	$$⊢T=\mathrm{2Ideal}\left(R\right)$$
Assertion	2idlelb	$$⊢U\in T\leftrightarrow \left(U\in I\wedge U\in J\right)$$

Proof

Step	Hyp	Ref	Expression
1		2idlel.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
2		2idlel.o	$$⊢O={opp}_r\left(R\right)$$
3		2idlel.j	$$⊢J=\mathrm{LIdeal}\left(O\right)$$
4		2idlel.t	$$⊢T=\mathrm{2Ideal}\left(R\right)$$
5	1 2 3 4	2idlval	$$⊢T=I\cap J$$
6	5	elin2	$$⊢U\in T\leftrightarrow \left(U\in I\wedge U\in J\right)$$