Metamath Proof Explorer

Theorem lidlacs

Description: The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses lidlacs.b 
|- B = ( Base ` W )
lidlacs.i 
|- I = ( LIdeal ` W )
Assertion lidlacs 
|- ( W e. Ring -> I e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 lidlacs.b 
 |-  B = ( Base ` W )
2 lidlacs.i 
 |-  I = ( LIdeal ` W )
3 lidlval 
 |-  ( LIdeal ` W ) = ( LSubSp ` ( ringLMod ` W ) )
4 2 3 eqtri 
 |-  I = ( LSubSp ` ( ringLMod ` W ) )
5 rlmlmod 
 |-  ( W e. Ring -> ( ringLMod ` W ) e. LMod )
6 rlmbas 
 |-  ( Base ` W ) = ( Base ` ( ringLMod ` W ) )
7 1 6 eqtri 
 |-  B = ( Base ` ( ringLMod ` W ) )
8 eqid 
 |-  ( LSubSp ` ( ringLMod ` W ) ) = ( LSubSp ` ( ringLMod ` W ) )
9 7 8 lssacs 
 |-  ( ( ringLMod ` W ) e. LMod -> ( LSubSp ` ( ringLMod ` W ) ) e. ( ACS ` B ) )
10 5 9 syl 
 |-  ( W e. Ring -> ( LSubSp ` ( ringLMod ` W ) ) e. ( ACS ` B ) )
11 4 10 eqeltrid 
 |-  ( W e. Ring -> I e. ( ACS ` B ) )