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	|- U = ( LIdeal ` R )
	rnglidl0.z	|- .0. = ( 0g ` R )
Assertion	lidl0	|- ( R e. Ring -> { .0. } e. U )

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	|- U = ( LIdeal ` R )
2		rnglidl0.z	|- .0. = ( 0g ` R )
3		ringrng	|- ( R e. Ring -> R e. Rng )
4	1 2	rnglidl0	|- ( R e. Rng -> { .0. } e. U )
5	3 4	syl	|- ( R e. Ring -> { .0. } e. U )