Theorem lidlnsg

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

	Ref	Expression
Assertion	lidlnsg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
2	1	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
3		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
4	3	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Abel )
5		ablnsg	⊢ ( 𝑅 ∈ Abel → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
6	4 5	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
7	2 6	eleqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )