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	$⊢ φ \to R \in Rng$
	rng2idlsubgsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlsubgsubrng.u	$⊢ φ \to I \in SubGrp (R)$
Assertion	rng2idlsubgsubrng	Could not format assertion : No typesetting found for \|- ( ph -> I e. ( SubRng ` R ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	$⊢ φ \to R \in Rng$
2		rng2idlsubgsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlsubgsubrng.u	$⊢ φ \to I \in 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 \in 2Ideal (R) \leftrightarrow (I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R)))$
9	8	simplbi	$⊢ I \in 2Ideal (R) \to I \in LIdeal (R)$
10	2 9	syl	$⊢ φ \to I \in LIdeal (R)$
11		eqid	$⊢ R ↾_{𝑠} I = R ↾_{𝑠} I$
12	4 11	rnglidlrng	$⊢ (R \in Rng \land I \in LIdeal (R) \land I \in SubGrp (R)) \to R ↾_{𝑠} I \in Rng$
13	1 10 3 12	syl3anc	$⊢ φ \to R ↾_{𝑠} I \in 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 \|-

Metamath Proof Explorer