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 T U I U 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 J
6 5 elin2 U T U I U J