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 Ring I 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 Ring ringLMod W 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 LMod LSubSp ringLMod W ACS B
10 5 9 syl W Ring LSubSp ringLMod W ACS B
11 4 10 eqeltrid W Ring I ACS B