Metamath Proof Explorer


Theorem lidlnsg

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

Ref Expression
Assertion lidlnsg
|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
2 1 lidlsubg
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
3 ringabl
 |-  ( R e. Ring -> R e. Abel )
4 3 adantr
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> R e. Abel )
5 ablnsg
 |-  ( R e. Abel -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
6 4 5 syl
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
7 2 6 eleqtrrd
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )