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 ) ) |
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 ) ) |