Theorem ply1mulr

Description: Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	ply1plusg.y	|- Y = ( Poly1 ` R )
	ply1plusg.s	|- S = ( 1o mPoly R )
	ply1mulr.n	|- .x. = ( .r ` Y )
Assertion	ply1mulr	|- .x. = ( .r ` S )

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	|- Y = ( Poly1 ` R )
2		ply1plusg.s	|- S = ( 1o mPoly R )
3		ply1mulr.n	|- .x. = ( .r ` Y )
4		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
5		eqid	|- ( .r ` S ) = ( .r ` S )
6	2 4 5	mplmulr	|- ( .r ` S ) = ( .r ` ( 1o mPwSer R ) )
7		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
8		eqid	|- ( .r ` ( PwSer1 ` R ) ) = ( .r ` ( PwSer1 ` R ) )
9	7 4 8	psr1mulr	|- ( .r ` ( PwSer1 ` R ) ) = ( .r ` ( 1o mPwSer R ) )
10		fvex	|- ( Base ` ( 1o mPoly R ) ) e. _V
11	1 7	ply1val	|- Y = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
12	11 8	ressmulr	|- ( ( Base ` ( 1o mPoly R ) ) e. _V -> ( .r ` ( PwSer1 ` R ) ) = ( .r ` Y ) )
13	10 12	ax-mp	|- ( .r ` ( PwSer1 ` R ) ) = ( .r ` Y )
14	6 9 13	3eqtr2i	|- ( .r ` S ) = ( .r ` Y )
15	3 14	eqtr4i	|- .x. = ( .r ` S )