Metamath Proof Explorer


Theorem rlmval

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

Ref Expression
Assertion rlmval ringLModW=subringAlgWBaseW

Proof

Step Hyp Ref Expression
1 fveq2 a=WsubringAlga=subringAlgW
2 fveq2 a=WBasea=BaseW
3 1 2 fveq12d a=WsubringAlgaBasea=subringAlgWBaseW
4 df-rgmod ringLMod=aVsubringAlgaBasea
5 fvex subringAlgWBaseWV
6 3 4 5 fvmpt WVringLModW=subringAlgWBaseW
7 0fv BaseW=
8 7 eqcomi =BaseW
9 fvprc ¬WVringLModW=
10 fvprc ¬WVsubringAlgW=
11 10 fveq1d ¬WVsubringAlgWBaseW=BaseW
12 8 9 11 3eqtr4a ¬WVringLModW=subringAlgWBaseW
13 6 12 pm2.61i ringLModW=subringAlgWBaseW