Theorem lidl0

Description: Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	rnglidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	rnglidl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		rnglidl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
4	1 2	rnglidl0	⊢ ( 𝑅 ∈ Rng → { 0 } ∈ 𝑈 )
5	3 4	syl	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )