Theorem lidlval

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

	Ref	Expression
Assertion	lidlval	⊢ ( LIdeal ‘ 𝑊 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		df-lidl	⊢ LIdeal = ( LSubSp ∘ ringLMod )
2	1	fveq1i	⊢ ( LIdeal ‘ 𝑊 ) = ( ( LSubSp ∘ ringLMod ) ‘ 𝑊 )
3		00lss	⊢ ∅ = ( LSubSp ‘ ∅ )
4		rlmfn	⊢ ringLMod Fn V
5		fnfun	⊢ ( ringLMod Fn V → Fun ringLMod )
6	4 5	ax-mp	⊢ Fun ringLMod
7	3 6	fvco4i	⊢ ( ( LSubSp ∘ ringLMod ) ‘ 𝑊 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )
8	2 7	eqtri	⊢ ( LIdeal ‘ 𝑊 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑊 ) )