Theorem lidl0

Description: Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidl0.u	|- U = ( LIdeal ` R )
	lidl0.z	|- .0. = ( 0g ` R )
Assertion	lidl0	|- ( R e. Ring -> { .0. } e. U )

Proof

Step	Hyp	Ref	Expression
1		lidl0.u	|- U = ( LIdeal ` R )
2		lidl0.z	|- .0. = ( 0g ` R )
3		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
4		rlm0	|- ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )
5	2 4	eqtri	|- .0. = ( 0g ` ( ringLMod ` R ) )
6		eqid	|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) )
7	5 6	lsssn0	|- ( ( ringLMod ` R ) e. LMod -> { .0. } e. ( LSubSp ` ( ringLMod ` R ) ) )
8	3 7	syl	|- ( R e. Ring -> { .0. } e. ( LSubSp ` ( ringLMod ` R ) ) )
9		lidlval	|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
10	1 9	eqtri	|- U = ( LSubSp ` ( ringLMod ` R ) )
11	8 10	eleqtrrdi	|- ( R e. Ring -> { .0. } e. U )