Theorem rng2idlsubg0

Description: The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlsubgsubrng.r	|- ( ph -> R e. Rng )
	rng2idlsubgsubrng.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlsubgsubrng.u	|- ( ph -> I e. ( SubGrp ` R ) )
Assertion	rng2idlsubg0	|- ( ph -> ( 0g ` R ) e. I )

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	|- ( ph -> R e. Rng )
2		rng2idlsubgsubrng.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlsubgsubrng.u	|- ( ph -> I e. ( SubGrp ` R ) )
4	1 2 3	rng2idlsubgsubrng	|- ( ph -> I e. ( SubRng ` R ) )
5		subrngsubg	|- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	6	subg0cl	|- ( I e. ( SubGrp ` R ) -> ( 0g ` R ) e. I )
8	4 5 7	3syl	|- ( ph -> ( 0g ` R ) e. I )