lidlnsg

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

		Ref	Expression
	Assertion	lidlnsg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in NrmSGrp (R)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ LIdeal (R) = LIdeal (R)$
2	1	lidlsubg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in SubGrp (R)$
3		ringabl	$⊢ R \in Ring \to R \in Abel$
4	3	adantr	$⊢ (R \in Ring \land I \in LIdeal (R)) \to R \in Abel$
5		ablnsg	$⊢ R \in Abel \to NrmSGrp (R) = SubGrp (R)$
6	4 5	syl	$⊢ (R \in Ring \land I \in LIdeal (R)) \to NrmSGrp (R) = SubGrp (R)$
7	2 6	eleqtrrd	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in NrmSGrp (R)$

Metamath Proof Explorer