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

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	$⊢ φ \to R \in Rng$
2		rng2idlsubgsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlsubgsubrng.u	$⊢ φ \to I \in SubGrp (R)$
4	1 2 3	rng2idlsubgsubrng	$⊢ φ \to I \in SubRng (R)$
5		subrngringnsg	$⊢ I \in SubRng (R) \to I \in NrmSGrp (R)$
6	4 5	syl	$⊢ φ \to I \in NrmSGrp (R)$