This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngansg

Description: Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025)

		Ref	Expression
	Assertion	rngansg	$⊢ R \in Rng \to NrmSGrp (R) = SubGrp (R)$

Step	Hyp	Ref	Expression
1		rngabl	$⊢ R \in Rng \to R \in Abel$
2		ablnsg	$⊢ R \in Abel \to NrmSGrp (R) = SubGrp (R)$
3	1 2	syl	$⊢ R \in Rng \to NrmSGrp (R) = SubGrp (R)$