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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	ply1plusg.s	⊢ 𝑆 = ( 1o mPoly 𝑅 )
	ply1mulr.n	⊢ · = ( .r ‘ 𝑌 )
Assertion	ply1mulr	⊢ · = ( .r ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		ply1plusg.s	⊢ 𝑆 = ( 1o mPoly 𝑅 )
3		ply1mulr.n	⊢ · = ( .r ‘ 𝑌 )
4		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
6	2 4 5	mplmulr	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
7		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8		eqid	⊢ ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ ( PwSer1 ‘ 𝑅 ) )
9	7 4 8	psr1mulr	⊢ ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
10		fvex	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
11	1 7	ply1val	⊢ 𝑌 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
12	11 8	ressmulr	⊢ ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ 𝑌 ) )
13	10 12	ax-mp	⊢ ( .r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( .r ‘ 𝑌 )
14	6 9 13	3eqtr2i	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑌 )
15	3 14	eqtr4i	⊢ · = ( .r ‘ 𝑆 )