Metamath Proof Explorer


Theorem rng2idlsubg0

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

Ref Expression
Hypotheses rng2idlsubgsubrng.r φ R Rng
rng2idlsubgsubrng.i φ I 2Ideal R
rng2idlsubgsubrng.u φ I SubGrp R
Assertion rng2idlsubg0 φ 0 R I

Proof

Step Hyp Ref Expression
1 rng2idlsubgsubrng.r φ R Rng
2 rng2idlsubgsubrng.i φ I 2Ideal R
3 rng2idlsubgsubrng.u φ I SubGrp R
4 1 2 3 rng2idlsubgsubrng 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