Theorem rng2idlsubrng

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

	Ref	Expression
Hypotheses	rng2idlsubrng.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlsubrng.u	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
Assertion	rng2idlsubrng	⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubrng.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rng2idlsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rng2idlsubrng.u	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
6	4 5	2idlss	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
8	4	issubrng	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐼 ) ∈ Rng ∧ 𝐼 ⊆ ( Base ‘ 𝑅 ) ) )
9	1 3 7 8	syl3anbrc	⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )