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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idlsubrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idlsubrng.u	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
Assertion	rng2idl0	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )

Proof

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