Metamath Proof Explorer


Theorem lidlnsg

Description: An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024)

Ref Expression
Assertion lidlnsg R Ring I LIdeal R I NrmSGrp R

Proof

Step Hyp Ref Expression
1 eqid LIdeal R = LIdeal R
2 1 lidlsubg R Ring I LIdeal R I SubGrp R
3 ringabl R Ring R Abel
4 3 adantr R Ring I LIdeal R R Abel
5 ablnsg R Abel NrmSGrp R = SubGrp R
6 4 5 syl R Ring I LIdeal R NrmSGrp R = SubGrp R
7 2 6 eleqtrrd R Ring I LIdeal R I NrmSGrp R