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	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
	lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion	lidlabl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2		lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
4	3	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑅 ∈ Abel )
5	1	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑈 ∈ ( SubGrp ‘ 𝑅 ) )
6	2	subgabl	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Abel )
7	4 5 6	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Abel )