Theorem lidl0ALT

Description: Alternate proof for lidl0 not using rnglidl0 : Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	|- U = ( LIdeal ` R )
2		rnglidl0.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 )