Step |
Hyp |
Ref |
Expression |
1 |
|
mpladd.p |
|- P = ( I mPoly R ) |
2 |
|
mpladd.b |
|- B = ( Base ` P ) |
3 |
|
mpladd.a |
|- .+ = ( +g ` R ) |
4 |
|
mpladd.g |
|- .+b = ( +g ` P ) |
5 |
|
mpladd.x |
|- ( ph -> X e. B ) |
6 |
|
mpladd.y |
|- ( ph -> Y e. B ) |
7 |
|
eqid |
|- ( I mPwSer R ) = ( I mPwSer R ) |
8 |
|
eqid |
|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) |
9 |
2
|
fvexi |
|- B e. _V |
10 |
1 7 2
|
mplval2 |
|- P = ( ( I mPwSer R ) |`s B ) |
11 |
|
eqid |
|- ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer R ) ) |
12 |
10 11
|
ressplusg |
|- ( B e. _V -> ( +g ` ( I mPwSer R ) ) = ( +g ` P ) ) |
13 |
9 12
|
ax-mp |
|- ( +g ` ( I mPwSer R ) ) = ( +g ` P ) |
14 |
4 13
|
eqtr4i |
|- .+b = ( +g ` ( I mPwSer R ) ) |
15 |
1 7 2 8
|
mplbasss |
|- B C_ ( Base ` ( I mPwSer R ) ) |
16 |
15 5
|
sselid |
|- ( ph -> X e. ( Base ` ( I mPwSer R ) ) ) |
17 |
15 6
|
sselid |
|- ( ph -> Y e. ( Base ` ( I mPwSer R ) ) ) |
18 |
7 8 3 14 16 17
|
psradd |
|- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) ) |