Metamath Proof Explorer

Theorem lidlrng

Description: A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020) (Proof shortened by AV, 11-Mar-2025)

Ref Expression
Hypotheses lidlabl.l ⊢ L = LIdeal ⁡ R
lidlabl.i ⊢ I = R ↾ 𝑠 U
Assertion lidlrng ⊢ R ∈ Ring ∧ U ∈ L → I ∈ Rng

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ L = LIdeal ⁡ R
2 lidlabl.i ⊢ I = R ↾ 𝑠 U
3 ringrng ⊢ R ∈ Ring → R ∈ Rng
4 3 adantr ⊢ R ∈ Ring ∧ U ∈ L → R ∈ Rng
5 simpr ⊢ R ∈ Ring ∧ U ∈ L → U ∈ L
6 1 lidlsubg ⊢ R ∈ Ring ∧ U ∈ L → U ∈ SubGrp ⁡ R
7 1 2 rnglidlrng ⊢ R ∈ Rng ∧ U ∈ L ∧ U ∈ SubGrp ⁡ R → I ∈ Rng
8 4 5 6 7 syl3anc ⊢ R ∈ Ring ∧ U ∈ L → I ∈ Rng