Step |
Hyp |
Ref |
Expression |
1 |
|
fvi |
|- ( R e. _V -> ( _I ` R ) = R ) |
2 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
3 |
2
|
ressid |
|- ( R e. _V -> ( R |`s ( Base ` R ) ) = R ) |
4 |
1 3
|
eqtr4d |
|- ( R e. _V -> ( _I ` R ) = ( R |`s ( Base ` R ) ) ) |
5 |
|
fvprc |
|- ( -. R e. _V -> ( _I ` R ) = (/) ) |
6 |
|
reldmress |
|- Rel dom |`s |
7 |
6
|
ovprc1 |
|- ( -. R e. _V -> ( R |`s ( Base ` R ) ) = (/) ) |
8 |
5 7
|
eqtr4d |
|- ( -. R e. _V -> ( _I ` R ) = ( R |`s ( Base ` R ) ) ) |
9 |
4 8
|
pm2.61i |
|- ( _I ` R ) = ( R |`s ( Base ` R ) ) |
10 |
|
rlmval |
|- ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) |
11 |
10
|
a1i |
|- ( T. -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) ) |
12 |
|
ssidd |
|- ( T. -> ( Base ` R ) C_ ( Base ` R ) ) |
13 |
11 12
|
srasca |
|- ( T. -> ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) ) |
14 |
13
|
mptru |
|- ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) |
15 |
9 14
|
eqtri |
|- ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) ) |