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