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 e. Ring -> B e. U )

Proof

Step Hyp Ref Expression
1 lidl0.u 
 |-  U = ( LIdeal ` R )
2 lidl1.b 
 |-  B = ( Base ` R )
3 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. 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 ) e. LMod -> B e. ( LSubSp ` ( ringLMod ` R ) ) )
8 3 7 syl 
 |-  ( R e. Ring -> B 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 -> B e. U )