Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Prime Ideals
lidlnsg
Next ⟩
cringm4
Metamath Proof Explorer
Ascii
Unicode
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