This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rng2idlsubgsubrng

Description: A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025)

Ref Expression
Hypotheses rng2idlsubgsubrng.r ⊢ φ → R ∈ Rng
rng2idlsubgsubrng.i ⊢ φ → I ∈ 2Ideal ⁡ R
rng2idlsubgsubrng.u ⊢ φ → I ∈ SubGrp ⁡ R
Assertion rng2idlsubgsubrng ⊢ φ → I ∈ SubRng ⁡ R

Proof

Step Hyp Ref Expression
1 rng2idlsubgsubrng.r ⊢ φ → R ∈ Rng
2 rng2idlsubgsubrng.i ⊢ φ → I ∈ 2Ideal ⁡ R
3 rng2idlsubgsubrng.u ⊢ φ → I ∈ SubGrp ⁡ R
4 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
5 eqid ⊢ opp r ⁡ R = opp r ⁡ R
6 eqid ⊢ LIdeal ⁡ opp r ⁡ R = LIdeal ⁡ opp r ⁡ R
7 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
8 4 5 6 7 2idlelb ⊢ I ∈ 2Ideal ⁡ R ↔ I ∈ LIdeal ⁡ R ∧ I ∈ LIdeal ⁡ opp r ⁡ R
9 8 simplbi ⊢ I ∈ 2Ideal ⁡ R → I ∈ LIdeal ⁡ R
10 2 9 syl ⊢ φ → I ∈ LIdeal ⁡ R
11 eqid ⊢ R ↾ 𝑠 I = R ↾ 𝑠 I
12 4 11 rnglidlrng ⊢ R ∈ Rng ∧ I ∈ LIdeal ⁡ R ∧ I ∈ SubGrp ⁡ R → R ↾ 𝑠 I ∈ Rng
13 1 10 3 12 syl3anc ⊢ φ → R ↾ 𝑠 I ∈ Rng
14 1 2 13 rng2idlsubrng ⊢ φ → I ∈ SubRng ⁡ R