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

Metamath Proof Explorer

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	$⊢ φ \to R \in Rng$
		rng2idlsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
		rng2idlsubrng.u	$⊢ φ \to R ↾_{𝑠} I \in Rng$
	Assertion	rng2idlsubrng	$⊢ φ \to I \in SubRng (R)$

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubrng.r	$⊢ φ \to R \in Rng$
2		rng2idlsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlsubrng.u	$⊢ φ \to R ↾_{𝑠} I \in Rng$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
6	4 5	2idlss	$⊢ I \in 2Ideal (R) \to I \subseteq {Base}_{R}$
7	2 6	syl	$⊢ φ \to I \subseteq {Base}_{R}$
8	4	issubrng	$⊢ I \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} I \in Rng \land I \subseteq {Base}_{R})$
9	1 3 7 8	syl3anbrc	$⊢ φ \to I \in SubRng (R)$