Step |
Hyp |
Ref |
Expression |
1 |
|
ressmpl.s |
|- S = ( I mPoly R ) |
2 |
|
ressmpl.h |
|- H = ( R |`s T ) |
3 |
|
ressmpl.u |
|- U = ( I mPoly H ) |
4 |
|
ressmpl.b |
|- B = ( Base ` U ) |
5 |
|
ressmpl.1 |
|- ( ph -> I e. V ) |
6 |
|
ressmpl.2 |
|- ( ph -> T e. ( SubRing ` R ) ) |
7 |
|
ressmpl.p |
|- P = ( S |`s B ) |
8 |
|
eqid |
|- ( I mPwSer H ) = ( I mPwSer H ) |
9 |
|
eqid |
|- ( Base ` ( I mPwSer H ) ) = ( Base ` ( I mPwSer H ) ) |
10 |
3 8 4 9
|
mplbasss |
|- B C_ ( Base ` ( I mPwSer H ) ) |
11 |
10
|
sseli |
|- ( X e. B -> X e. ( Base ` ( I mPwSer H ) ) ) |
12 |
10
|
sseli |
|- ( Y e. B -> Y e. ( Base ` ( I mPwSer H ) ) ) |
13 |
11 12
|
anim12i |
|- ( ( X e. B /\ Y e. B ) -> ( X e. ( Base ` ( I mPwSer H ) ) /\ Y e. ( Base ` ( I mPwSer H ) ) ) ) |
14 |
|
eqid |
|- ( I mPwSer R ) = ( I mPwSer R ) |
15 |
|
eqid |
|- ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) = ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) |
16 |
14 2 8 9 15 6
|
resspsradd |
|- ( ( ph /\ ( X e. ( Base ` ( I mPwSer H ) ) /\ Y e. ( Base ` ( I mPwSer H ) ) ) ) -> ( X ( +g ` ( I mPwSer H ) ) Y ) = ( X ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) ) |
17 |
13 16
|
sylan2 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` ( I mPwSer H ) ) Y ) = ( X ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) ) |
18 |
4
|
fvexi |
|- B e. _V |
19 |
3 8 4
|
mplval2 |
|- U = ( ( I mPwSer H ) |`s B ) |
20 |
|
eqid |
|- ( +g ` ( I mPwSer H ) ) = ( +g ` ( I mPwSer H ) ) |
21 |
19 20
|
ressplusg |
|- ( B e. _V -> ( +g ` ( I mPwSer H ) ) = ( +g ` U ) ) |
22 |
18 21
|
ax-mp |
|- ( +g ` ( I mPwSer H ) ) = ( +g ` U ) |
23 |
22
|
oveqi |
|- ( X ( +g ` ( I mPwSer H ) ) Y ) = ( X ( +g ` U ) Y ) |
24 |
|
fvex |
|- ( Base ` S ) e. _V |
25 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
26 |
1 14 25
|
mplval2 |
|- S = ( ( I mPwSer R ) |`s ( Base ` S ) ) |
27 |
|
eqid |
|- ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer R ) ) |
28 |
26 27
|
ressplusg |
|- ( ( Base ` S ) e. _V -> ( +g ` ( I mPwSer R ) ) = ( +g ` S ) ) |
29 |
24 28
|
ax-mp |
|- ( +g ` ( I mPwSer R ) ) = ( +g ` S ) |
30 |
|
fvex |
|- ( Base ` ( I mPwSer H ) ) e. _V |
31 |
15 27
|
ressplusg |
|- ( ( Base ` ( I mPwSer H ) ) e. _V -> ( +g ` ( I mPwSer R ) ) = ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) ) |
32 |
30 31
|
ax-mp |
|- ( +g ` ( I mPwSer R ) ) = ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) |
33 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
34 |
7 33
|
ressplusg |
|- ( B e. _V -> ( +g ` S ) = ( +g ` P ) ) |
35 |
18 34
|
ax-mp |
|- ( +g ` S ) = ( +g ` P ) |
36 |
29 32 35
|
3eqtr3i |
|- ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) = ( +g ` P ) |
37 |
36
|
oveqi |
|- ( X ( +g ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) = ( X ( +g ` P ) Y ) |
38 |
17 23 37
|
3eqtr3g |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) ) |