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={\mathrm{Base}}_W$$
	lidlacs.i	$$⊢I=\mathrm{LIdeal}\left(W\right)$$
Assertion	lidlacs	$$⊢W\in \mathrm{Ring}\to I\in \mathrm{ACS}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lidlacs.b	$$⊢B={\mathrm{Base}}_W$$
2		lidlacs.i	$$⊢I=\mathrm{LIdeal}\left(W\right)$$
3		lidlval	$$⊢\mathrm{LIdeal}\left(W\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$
4	2 3	eqtri	$$⊢I=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$
5		rlmlmod	$$⊢W\in \mathrm{Ring}\to \mathrm{ringLMod}\left(W\right)\in \mathrm{LMod}$$
6		rlmbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_{\mathrm{ringLMod}\left(W\right)}$$
7	1 6	eqtri	$$⊢B={\mathrm{Base}}_{\mathrm{ringLMod}\left(W\right)}$$
8		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$
9	7 8	lssacs	$$⊢\mathrm{ringLMod}\left(W\right)\in \mathrm{LMod}\to \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)\in \mathrm{ACS}\left(B\right)$$
10	5 9	syl	$$⊢W\in \mathrm{Ring}\to \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)\in \mathrm{ACS}\left(B\right)$$
11	4 10	eqeltrid	$$⊢W\in \mathrm{Ring}\to I\in \mathrm{ACS}\left(B\right)$$