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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlsubgsubrng.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlsubgsubrng.u	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
Assertion	rng2idlsubgnsg	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlsubgsubrng.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlsubgsubrng.u	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
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	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$