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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlsubgsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlsubgsubrng.u	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
Assertion	rng2idlsubg0	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rng2idlsubgsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rng2idlsubgsubrng.u	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
4	1 2 3	rng2idlsubgsubrng	⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )
5		subrngsubg	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7	6	subg0cl	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
8	4 5 7	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )