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 = ( oppR ` R ) |
||
| 2idlel.j | |- J = ( LIdeal ` O ) |
||
| 2idlel.t | |- T = ( 2Ideal ` R ) |
||
| Assertion | 2idlelb | |- ( U e. T <-> ( U e. I /\ U e. J ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2idlel.i | |- I = ( LIdeal ` R ) |
|
| 2 | 2idlel.o | |- O = ( oppR ` R ) |
|
| 3 | 2idlel.j | |- J = ( LIdeal ` O ) |
|
| 4 | 2idlel.t | |- T = ( 2Ideal ` R ) |
|
| 5 | 1 2 3 4 | 2idlval | |- T = ( I i^i J ) |
| 6 | 5 | elin2 | |- ( U e. T <-> ( U e. I /\ U e. J ) ) |