Metamath Proof Explorer


Theorem ressply1add

Description: A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressply1.s
|- S = ( Poly1 ` R )
ressply1.h
|- H = ( R |`s T )
ressply1.u
|- U = ( Poly1 ` H )
ressply1.b
|- B = ( Base ` U )
ressply1.2
|- ( ph -> T e. ( SubRing ` R ) )
ressply1.p
|- P = ( S |`s B )
Assertion ressply1add
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) )

Proof

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 ) )