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