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

Metamath Proof Explorer

Theorem lidlval

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

		Ref	Expression
	Assertion	lidlval	$⊢ LIdeal (W) = LSubSp (ringLMod (W))$

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