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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlsubrng.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlsubrng.u	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
Assertion	rng2idlsubrng	Could not format assertion : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubrng.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlsubrng.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlsubrng.u	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
6	4 5	2idlss	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to I\subseteq {\mathrm{Base}}_R$$
7	2 6	syl	$$⊢\phi \to I\subseteq {\mathrm{Base}}_R$$
8	4	issubrng	Could not format ( I e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s I ) e. Rng /\ I C_ ( Base ` R ) ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s I ) e. Rng /\ I C_ ( Base ` R ) ) ) with typecode |-
9	1 3 7 8	syl3anbrc	Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-