Metamath Proof Explorer


Theorem rng2idlsubgnsg

Description: A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal 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 rng2idlsubgnsg φ I NrmSGrp R

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 subrngringnsg Could not format ( I e. ( SubRng ` R ) -> I e. ( NrmSGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( NrmSGrp ` R ) ) with typecode |-
6 4 5 syl φ I NrmSGrp R