This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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