Metamath Proof Explorer

Theorem rlmval

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

Ref Expression
Assertion rlmval 
|- ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = W -> ( subringAlg ` a ) = ( subringAlg ` W ) )
2 fveq2 
 |-  ( a = W -> ( Base ` a ) = ( Base ` W ) )
3 1 2 fveq12d 
 |-  ( a = W -> ( ( subringAlg ` a ) ` ( Base ` a ) ) = ( ( subringAlg ` W ) ` ( Base ` W ) ) )
4 df-rgmod 
 |-  ringLMod = ( a e. _V |-> ( ( subringAlg ` a ) ` ( Base ` a ) ) )
5 fvex 
 |-  ( ( subringAlg ` W ) ` ( Base ` W ) ) e. _V
6 3 4 5 fvmpt 
 |-  ( W e. _V -> ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) ) )
7 0fv 
 |-  ( (/) ` ( Base ` W ) ) = (/)
8 7 eqcomi 
 |-  (/) = ( (/) ` ( Base ` W ) )
9 fvprc 
 |-  ( -. W e. _V -> ( ringLMod ` W ) = (/) )
10 fvprc 
 |-  ( -. W e. _V -> ( subringAlg ` W ) = (/) )
11 10 fveq1d 
 |-  ( -. W e. _V -> ( ( subringAlg ` W ) ` ( Base ` W ) ) = ( (/) ` ( Base ` W ) ) )
12 8 9 11 3eqtr4a 
 |-  ( -. W e. _V -> ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) ) )
13 6 12 pm2.61i 
 |-  ( ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) )