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