Metamath Proof Explorer

Theorem lidl0cl

Description: An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlcl.u 
|- U = ( LIdeal ` R )
lidl0cl.z 
|- .0. = ( 0g ` R )
Assertion lidl0cl 
|- ( ( R e. Ring /\ I e. U ) -> .0. e. I )

Proof

Step Hyp Ref Expression
1 lidlcl.u 
 |-  U = ( LIdeal ` R )
2 lidl0cl.z 
 |-  .0. = ( 0g ` R )
3 rlm0 
 |-  ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )
4 2 3 eqtri 
 |-  .0. = ( 0g ` ( ringLMod ` R ) )
5 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
6 simpr 
 |-  ( ( R e. Ring /\ I e. U ) -> I e. U )
7 lidlval 
 |-  ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
8 1 7 eqtri 
 |-  U = ( LSubSp ` ( ringLMod ` R ) )
9 6 8 eleqtrdi 
 |-  ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
10 eqid 
 |-  ( 0g ` ( ringLMod ` R ) ) = ( 0g ` ( ringLMod ` R ) )
11 eqid 
 |-  ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) )
12 10 11 lss0cl 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) -> ( 0g ` ( ringLMod ` R ) ) e. I )
13 5 9 12 syl2an2r 
 |-  ( ( R e. Ring /\ I e. U ) -> ( 0g ` ( ringLMod ` R ) ) e. I )
14 4 13 eqeltrid 
 |-  ( ( R e. Ring /\ I e. U ) -> .0. e. I )