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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlsubgsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlsubgsubrng.u	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
Assertion	rng2idlsubgnsg	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rng2idlsubgsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rng2idlsubgsubrng.u	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
4	1 2 3	rng2idlsubgsubrng	⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )
5		subrngringnsg	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
6	4 5	syl	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )