Description: Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | rlmval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |
|
2 | fveq2 | |
|
3 | 1 2 | fveq12d | |
4 | df-rgmod | |
|
5 | fvex | |
|
6 | 3 4 5 | fvmpt | |
7 | 0fv | |
|
8 | 7 | eqcomi | |
9 | fvprc | |
|
10 | fvprc | |
|
11 | 10 | fveq1d | |
12 | 8 9 11 | 3eqtr4a | |
13 | 6 12 | pm2.61i | |