Metamath Proof Explorer

Theorem lidlabl

Description: A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020)

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		ringabl	$⊢ R \in Ring \to R \in Abel$
4	3	adantr	$⊢ (R \in Ring \land U \in L) \to R \in Abel$
5	1	lidlsubg	$⊢ (R \in Ring \land U \in L) \to U \in SubGrp (R)$
6	2	subgabl	$⊢ (R \in Abel \land U \in SubGrp (R)) \to I \in Abel$
7	4 5 6	syl2anc	$⊢ (R \in Ring \land U \in L) \to I \in Abel$