Theorem lidl1

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

	Ref	Expression
Hypotheses	lidl0.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
	lidl1.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	lidl1	$$⊢R\in \mathrm{Ring}\to B\in U$$

Proof

Step	Hyp	Ref	Expression
1		lidl0.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
2		lidl1.b	$$⊢B={\mathrm{Base}}_R$$
3		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
4		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
5	2 4	eqtri	$$⊢B={\mathrm{Base}}_{\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	lss1	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\to B\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	3 7	syl	$$⊢R\in \mathrm{Ring}\to B\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 B\in U$$