Metamath Proof Explorer


Theorem rng2idl0

Description: The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025)

Ref Expression
Hypotheses rng2idlsubrng.r φ R Rng
rng2idlsubrng.i φ I 2Ideal R
rng2idlsubrng.u φ R 𝑠 I Rng
Assertion rng2idl0 φ 0 R I

Proof

Step Hyp Ref Expression
1 rng2idlsubrng.r φ R Rng
2 rng2idlsubrng.i φ I 2Ideal R
3 rng2idlsubrng.u φ R 𝑠 I Rng
4 1 2 3 rng2idlsubrng Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-
5 subrngsubg Could not format ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) with typecode |-
6 eqid 0 R = 0 R
7 6 subg0cl I SubGrp R 0 R I
8 4 5 7 3syl φ 0 R I