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 Could not format assertion : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-

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 Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-