Description: A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025) (Revised by AV, 11-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | rng2idlsubrng.r | |- ( ph -> R e. Rng ) |
|
| rng2idlsubrng.i | |- ( ph -> I e. ( 2Ideal ` R ) ) |
||
| rng2idlsubrng.u | |- ( ph -> ( R |`s I ) e. Rng ) |
||
| Assertion | rng2idlsubrng | |- ( ph -> I e. ( SubRng ` R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rng2idlsubrng.r | |- ( ph -> R e. Rng ) |
|
| 2 | rng2idlsubrng.i | |- ( ph -> I e. ( 2Ideal ` R ) ) |
|
| 3 | rng2idlsubrng.u | |- ( ph -> ( R |`s I ) e. Rng ) |
|
| 4 | eqid | |- ( Base ` R ) = ( Base ` R ) |
|
| 5 | eqid | |- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
|
| 6 | 4 5 | 2idlss | |- ( I e. ( 2Ideal ` R ) -> I C_ ( Base ` R ) ) |
| 7 | 2 6 | syl | |- ( ph -> I C_ ( Base ` R ) ) |
| 8 | 4 | issubrng | |- ( I e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s I ) e. Rng /\ I C_ ( Base ` R ) ) ) |
| 9 | 1 3 7 8 | syl3anbrc | |- ( ph -> I e. ( SubRng ` R ) ) |