Metamath Proof Explorer

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 ↾ 𝑠 U
Assertion lidlabl ⊢ R ∈ Ring ∧ U ∈ L → I ∈ Abel

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ L = LIdeal ⁡ R
2 lidlabl.i ⊢ I = R ↾ 𝑠 U
3 ringabl ⊢ R ∈ Ring → R ∈ Abel
4 3 adantr ⊢ R ∈ Ring ∧ U ∈ L → R ∈ Abel
5 1 lidlsubg ⊢ R ∈ Ring ∧ U ∈ L → U ∈ SubGrp ⁡ R
6 2 subgabl ⊢ R ∈ Abel ∧ U ∈ SubGrp ⁡ R → I ∈ Abel
7 4 5 6 syl2anc ⊢ R ∈ Ring ∧ U ∈ L → I ∈ Abel