Theorem ressply1mul

Description: A restricted polynomial algebra has the same multiplication 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	ressply1mul	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` 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	ressmplmul	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` ( 1o mPoly H ) ) Y ) = ( X ( .r ` ( ( 1o mPoly R ) |`s B ) ) Y ) )
14		eqid	|- ( .r ` U ) = ( .r ` U )
15	3 8 14	ply1mulr	|- ( .r ` U ) = ( .r ` ( 1o mPoly H ) )
16	15	oveqi	|- ( X ( .r ` U ) Y ) = ( X ( .r ` ( 1o mPoly H ) ) Y )
17		eqid	|- ( .r ` S ) = ( .r ` S )
18	1 7 17	ply1mulr	|- ( .r ` S ) = ( .r ` ( 1o mPoly R ) )
19	4	fvexi	|- B e. _V
20	6 17	ressmulr	|- ( B e. _V -> ( .r ` S ) = ( .r ` P ) )
21	19 20	ax-mp	|- ( .r ` S ) = ( .r ` P )
22		eqid	|- ( .r ` ( 1o mPoly R ) ) = ( .r ` ( 1o mPoly R ) )
23	12 22	ressmulr	|- ( B e. _V -> ( .r ` ( 1o mPoly R ) ) = ( .r ` ( ( 1o mPoly R ) |`s B ) ) )
24	19 23	ax-mp	|- ( .r ` ( 1o mPoly R ) ) = ( .r ` ( ( 1o mPoly R ) |`s B ) )
25	18 21 24	3eqtr3i	|- ( .r ` P ) = ( .r ` ( ( 1o mPoly R ) |`s B ) )
26	25	oveqi	|- ( X ( .r ` P ) Y ) = ( X ( .r ` ( ( 1o mPoly R ) |`s B ) ) Y )
27	13 16 26	3eqtr4g	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )