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 ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rng2idlsubgsubrng.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rng2idlsubgsubrng.u ⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
Assertion rng2idlsubgsubrng ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rng2idlsubgsubrng.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rng2idlsubgsubrng.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rng2idlsubgsubrng.u ⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
7 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
8 4 5 6 7 2idlelb ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
9 8 simplbi ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
10 2 9 syl ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
11 eqid ⊢ ( 𝑅 ↾s 𝐼 ) = ( 𝑅 ↾s 𝐼 )
12 4 11 rnglidlrng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
13 1 10 3 12 syl3anc ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
14 1 2 13 rng2idlsubrng ⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )