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 ‘ 𝐵 ) )