Step |
Hyp |
Ref |
Expression |
1 |
|
mplsca.p |
|- P = ( I mPoly R ) |
2 |
|
mplsca.i |
|- ( ph -> I e. V ) |
3 |
|
mplsca.r |
|- ( ph -> R e. W ) |
4 |
|
eqid |
|- ( I mPwSer R ) = ( I mPwSer R ) |
5 |
4 2 3
|
psrsca |
|- ( ph -> R = ( Scalar ` ( I mPwSer R ) ) ) |
6 |
|
fvex |
|- ( Base ` P ) e. _V |
7 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
8 |
1 4 7
|
mplval2 |
|- P = ( ( I mPwSer R ) |`s ( Base ` P ) ) |
9 |
|
eqid |
|- ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` ( I mPwSer R ) ) |
10 |
8 9
|
resssca |
|- ( ( Base ` P ) e. _V -> ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` P ) ) |
11 |
6 10
|
ax-mp |
|- ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` P ) |
12 |
5 11
|
eqtrdi |
|- ( ph -> R = ( Scalar ` P ) ) |