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 ‘ 𝑅 ) )