Step |
Hyp |
Ref |
Expression |
1 |
|
ressply1.s |
|- S = ( Poly1 ` R ) |
2 |
|
ressply1.h |
|- H = ( R |`s T ) |
3 |
|
ressply1.u |
|- U = ( Poly1 ` H ) |
4 |
|
ressply1.b |
|- B = ( Base ` U ) |
5 |
|
ressply1.2 |
|- ( ph -> T e. ( SubRing ` R ) ) |
6 |
|
ressply1.p |
|- P = ( S |`s B ) |
7 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
8 |
|
eqid |
|- ( 1o mPoly H ) = ( 1o mPoly H ) |
9 |
3 4
|
ply1bas |
|- B = ( Base ` ( 1o mPoly H ) ) |
10 |
|
1on |
|- 1o e. On |
11 |
10
|
a1i |
|- ( ph -> 1o e. On ) |
12 |
|
eqid |
|- ( ( 1o mPoly R ) |`s B ) = ( ( 1o mPoly R ) |`s B ) |
13 |
7 2 8 9 11 5 12
|
ressmpladd |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` ( 1o mPoly H ) ) Y ) = ( X ( +g ` ( ( 1o mPoly R ) |`s B ) ) Y ) ) |
14 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
15 |
3 8 14
|
ply1plusg |
|- ( +g ` U ) = ( +g ` ( 1o mPoly H ) ) |
16 |
15
|
oveqi |
|- ( X ( +g ` U ) Y ) = ( X ( +g ` ( 1o mPoly H ) ) Y ) |
17 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
18 |
1 7 17
|
ply1plusg |
|- ( +g ` S ) = ( +g ` ( 1o mPoly R ) ) |
19 |
4
|
fvexi |
|- B e. _V |
20 |
6 17
|
ressplusg |
|- ( B e. _V -> ( +g ` S ) = ( +g ` P ) ) |
21 |
19 20
|
ax-mp |
|- ( +g ` S ) = ( +g ` P ) |
22 |
|
eqid |
|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly R ) ) |
23 |
12 22
|
ressplusg |
|- ( B e. _V -> ( +g ` ( 1o mPoly R ) ) = ( +g ` ( ( 1o mPoly R ) |`s B ) ) ) |
24 |
19 23
|
ax-mp |
|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( ( 1o mPoly R ) |`s B ) ) |
25 |
18 21 24
|
3eqtr3i |
|- ( +g ` P ) = ( +g ` ( ( 1o mPoly R ) |`s B ) ) |
26 |
25
|
oveqi |
|- ( X ( +g ` P ) Y ) = ( X ( +g ` ( ( 1o mPoly R ) |`s B ) ) Y ) |
27 |
13 16 26
|
3eqtr4g |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) ) |