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 ( 𝜑𝑅 ∈ 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 ‘ 𝑅 ) )