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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
lidlacs.i ⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
Assertion lidlacs ( 𝑊 ∈ Ring → 𝐼 ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 lidlacs.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lidlacs.i ⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
3 lidlval ⊢ ( LIdeal ‘ 𝑊 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
4 2 3 eqtri ⊢ 𝐼 = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
5 rlmlmod ⊢ ( 𝑊 ∈ Ring → ( ringLMod ‘ 𝑊 ) ∈ LMod )
6 rlmbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( ringLMod ‘ 𝑊 ) )
7 1 6 eqtri ⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑊 ) )
8 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
9 7 8 lssacs ⊢ ( ( ringLMod ‘ 𝑊 ) ∈ LMod → ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) ) ∈ ( ACS ‘ 𝐵 ) )
10 5 9 syl ⊢ ( 𝑊 ∈ Ring → ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) ) ∈ ( ACS ‘ 𝐵 ) )
11 4 10 eqeltrid ⊢ ( 𝑊 ∈ Ring → 𝐼 ∈ ( ACS ‘ 𝐵 ) )