Metamath Proof Explorer


Theorem lidl1

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

Ref Expression
Hypotheses lidl0.u U = LIdeal R
lidl1.b B = Base R
Assertion lidl1 R Ring B U

Proof

Step Hyp Ref Expression
1 lidl0.u U = LIdeal R
2 lidl1.b B = Base R
3 rlmlmod R Ring ringLMod R LMod
4 rlmbas Base R = Base ringLMod R
5 2 4 eqtri B = Base ringLMod R
6 eqid LSubSp ringLMod R = LSubSp ringLMod R
7 5 6 lss1 ringLMod R LMod B LSubSp ringLMod R
8 3 7 syl R Ring B LSubSp ringLMod R
9 lidlval LIdeal R = LSubSp ringLMod R
10 1 9 eqtri U = LSubSp ringLMod R
11 8 10 eleqtrrdi R Ring B U