Theorem lidlabl

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

	Ref	Expression
Hypotheses	lidlabl.l	|- L = ( LIdeal ` R )
	lidlabl.i	|- I = ( R |`s U )
Assertion	lidlabl	|- ( ( R e. Ring /\ U e. L ) -> I e. Abel )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	|- L = ( LIdeal ` R )
2		lidlabl.i	|- I = ( R |`s U )
3		ringabl	|- ( R e. Ring -> R e. Abel )
4	3	adantr	|- ( ( R e. Ring /\ U e. L ) -> R e. Abel )
5	1	lidlsubg	|- ( ( R e. Ring /\ U e. L ) -> U e. ( SubGrp ` R ) )
6	2	subgabl	|- ( ( R e. Abel /\ U e. ( SubGrp ` R ) ) -> I e. Abel )
7	4 5 6	syl2anc	|- ( ( R e. Ring /\ U e. L ) -> I e. Abel )