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 e. Rng -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )

Proof

Step Hyp Ref Expression
1 rngabl 
 |-  ( R e. Rng -> R e. Abel )
2 ablnsg 
 |-  ( R e. Abel -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
3 1 2 syl 
 |-  ( R e. Rng -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )