Metamath Proof Explorer


Theorem rng2idlnsg

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

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 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