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=\mathrm{LIdeal}\left(R\right)$$
	rnglidl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	lidl0ALT	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in U$$

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
2		rnglidl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
4		rlm0	$$⊢0_R=0_{\mathrm{ringLMod}\left(R\right)}$$
5	2 4	eqtri	$$⊢\underset{\dot{}}{0}=0_{\mathrm{ringLMod}\left(R\right)}$$
6		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
7	5 6	lsssn0	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	3 7	syl	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
9		lidlval	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
10	1 9	eqtri	$$⊢U=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
11	8 10	eleqtrrdi	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in U$$