Theorem rng2idl0

Description: The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-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	rng2idl0	$$⊢\phi \to 0_R\in I$$

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	1 2 3	rng2idlsubrng	Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-
5		subrngsubg	Could not format ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) with typecode |-
6		eqid	$$⊢0_R=0_R$$
7	6	subg0cl	$$⊢I\in \mathrm{SubGrp}\left(R\right)\to 0_R\in I$$
8	4 5 7	3syl	$$⊢\phi \to 0_R\in I$$