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		eqid	|- ( PwSer1 ` H ) = ( PwSer1 ` H )
10	3 9 4	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
11		1on	|- 1o e. On
12	11	a1i	|- ( ph -> 1o e. On )
13		eqid	|- ( ( 1o mPoly R ) |`s B ) = ( ( 1o mPoly R ) |`s B )
14	7 2 8 10 12 5 13	ressmpladd	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` ( 1o mPoly H ) ) Y ) = ( X ( +g ` ( ( 1o mPoly R ) |`s B ) ) Y ) )
15		eqid	|- ( +g ` U ) = ( +g ` U )
16	3 8 15	ply1plusg	|- ( +g ` U ) = ( +g ` ( 1o mPoly H ) )
17	16	oveqi	|- ( X ( +g ` U ) Y ) = ( X ( +g ` ( 1o mPoly H ) ) Y )
18		eqid	|- ( +g ` S ) = ( +g ` S )
19	1 7 18	ply1plusg	|- ( +g ` S ) = ( +g ` ( 1o mPoly R ) )
20	4	fvexi	|- B e. _V
21	6 18	ressplusg	|- ( B e. _V -> ( +g ` S ) = ( +g ` P ) )
22	20 21	ax-mp	|- ( +g ` S ) = ( +g ` P )
23		eqid	|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly R ) )
24	13 23	ressplusg	|- ( B e. _V -> ( +g ` ( 1o mPoly R ) ) = ( +g ` ( ( 1o mPoly R ) |`s B ) ) )
25	20 24	ax-mp	|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( ( 1o mPoly R ) |`s B ) )
26	19 22 25	3eqtr3i	|- ( +g ` P ) = ( +g ` ( ( 1o mPoly R ) |`s B ) )
27	26	oveqi	|- ( X ( +g ` P ) Y ) = ( X ( +g ` ( ( 1o mPoly R ) |`s B ) ) Y )
28	14 17 27	3eqtr4g	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) )