Theorem lidlval

Description: Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	lidlval	$$⊢\mathrm{LIdeal}\left(W\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-lidl	$$⊢\mathrm{LIdeal}=\mathrm{LSubSp}\circ \mathrm{ringLMod}$$
2	1	fveq1i	$$⊢\mathrm{LIdeal}\left(W\right)=\left(\mathrm{LSubSp}\circ \mathrm{ringLMod}\right)\left(W\right)$$
3		00lss	$$⊢\varnothing =\mathrm{LSubSp}\left(\varnothing \right)$$
4		rlmfn	$$⊢\mathrm{ringLMod}Fn\mathrm{V}$$
5		fnfun	$$⊢\mathrm{ringLMod}Fn\mathrm{V}\to \mathrm{Fun}\mathrm{ringLMod}$$
6	4 5	ax-mp	$$⊢\mathrm{Fun}\mathrm{ringLMod}$$
7	3 6	fvco4i	$$⊢\left(\mathrm{LSubSp}\circ \mathrm{ringLMod}\right)\left(W\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$
8	2 7	eqtri	$$⊢\mathrm{LIdeal}\left(W\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(W\right)\right)$$