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 |
|- ( Y e. B -> Y e. ( Base ` ( I mPwSer H ) ) ) |
12 |
|
eqid |
|- ( I mPwSer R ) = ( I mPwSer R ) |
13 |
|
eqid |
|- ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) = ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) |
14 |
12 2 8 9 13 6
|
resspsrvsca |
|- ( ( ph /\ ( X e. T /\ Y e. ( Base ` ( I mPwSer H ) ) ) ) -> ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) ) |
15 |
11 14
|
sylanr2 |
|- ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) ) |
16 |
4
|
fvexi |
|- B e. _V |
17 |
3 8 4
|
mplval2 |
|- U = ( ( I mPwSer H ) |`s B ) |
18 |
|
eqid |
|- ( .s ` ( I mPwSer H ) ) = ( .s ` ( I mPwSer H ) ) |
19 |
17 18
|
ressvsca |
|- ( B e. _V -> ( .s ` ( I mPwSer H ) ) = ( .s ` U ) ) |
20 |
16 19
|
ax-mp |
|- ( .s ` ( I mPwSer H ) ) = ( .s ` U ) |
21 |
20
|
oveqi |
|- ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` U ) Y ) |
22 |
|
fvex |
|- ( Base ` S ) e. _V |
23 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
24 |
1 12 23
|
mplval2 |
|- S = ( ( I mPwSer R ) |`s ( Base ` S ) ) |
25 |
|
eqid |
|- ( .s ` ( I mPwSer R ) ) = ( .s ` ( I mPwSer R ) ) |
26 |
24 25
|
ressvsca |
|- ( ( Base ` S ) e. _V -> ( .s ` ( I mPwSer R ) ) = ( .s ` S ) ) |
27 |
22 26
|
ax-mp |
|- ( .s ` ( I mPwSer R ) ) = ( .s ` S ) |
28 |
|
fvex |
|- ( Base ` ( I mPwSer H ) ) e. _V |
29 |
13 25
|
ressvsca |
|- ( ( Base ` ( I mPwSer H ) ) e. _V -> ( .s ` ( I mPwSer R ) ) = ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) ) |
30 |
28 29
|
ax-mp |
|- ( .s ` ( I mPwSer R ) ) = ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) |
31 |
|
eqid |
|- ( .s ` S ) = ( .s ` S ) |
32 |
7 31
|
ressvsca |
|- ( B e. _V -> ( .s ` S ) = ( .s ` P ) ) |
33 |
16 32
|
ax-mp |
|- ( .s ` S ) = ( .s ` P ) |
34 |
27 30 33
|
3eqtr3i |
|- ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) = ( .s ` P ) |
35 |
34
|
oveqi |
|- ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) = ( X ( .s ` P ) Y ) |
36 |
15 21 35
|
3eqtr3g |
|- ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) ) |