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

Proof

Step Hyp Ref Expression
1 df-lidl
 |-  LIdeal = ( LSubSp o. ringLMod )
2 1 fveq1i
 |-  ( LIdeal ` W ) = ( ( LSubSp o. ringLMod ) ` W )
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 o. ringLMod ) ` W ) = ( LSubSp ` ( ringLMod ` W ) )
8 2 7 eqtri
 |-  ( LIdeal ` W ) = ( LSubSp ` ( ringLMod ` W ) )