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	|- ( ph -> R e. Rng )
	rng2idlsubrng.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlsubrng.u	|- ( ph -> ( R |`s I ) e. Rng )
Assertion	rng2idlnsg	|- ( ph -> I e. ( NrmSGrp ` R ) )

Proof

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	1 2 3	rng2idlsubrng	|- ( ph -> I e. ( SubRng ` R ) )
5		subrngringnsg	|- ( I e. ( SubRng ` R ) -> I e. ( NrmSGrp ` R ) )
6	4 5	syl	|- ( ph -> I e. ( NrmSGrp ` R ) )