This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = LIdeal (R)$
	2idlel.o	$⊢ O = {opp}_{r} (R)$
	2idlel.j	$⊢ J = LIdeal (O)$
	2idlel.t	$⊢ T = 2Ideal (R)$
Assertion	2idlelb	$⊢ U \in T \leftrightarrow (U \in I \land U \in J)$

Proof

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