Metamath Proof Explorer


Theorem lidl1ALT

Description: Alternate proof for lidl1 not using rnglidl1 : Every ring contains a unit 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
rnglidl1.b B = Base R
Assertion lidl1ALT R Ring B U

Proof

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