Theorem ply1opprmul

Description: Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1opprmul.y	|- Y = ( Poly1 ` R )
	ply1opprmul.s	|- S = ( oppR ` R )
	ply1opprmul.z	|- Z = ( Poly1 ` S )
	ply1opprmul.t	|- .x. = ( .r ` Y )
	ply1opprmul.u	|- .xb = ( .r ` Z )
	ply1opprmul.b	|- B = ( Base ` Y )
Assertion	ply1opprmul	|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )

Proof

Step	Hyp	Ref	Expression
1		ply1opprmul.y	|- Y = ( Poly1 ` R )
2		ply1opprmul.s	|- S = ( oppR ` R )
3		ply1opprmul.z	|- Z = ( Poly1 ` S )
4		ply1opprmul.t	|- .x. = ( .r ` Y )
5		ply1opprmul.u	|- .xb = ( .r ` Z )
6		ply1opprmul.b	|- B = ( Base ` Y )
7		id	|- ( R e. Ring -> R e. Ring )
8	1 6	ply1bascl	|- ( F e. B -> F e. ( Base ` ( PwSer1 ` R ) ) )
9		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
10		eqid	|- ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
11	9 10	psr1bascl	|- ( F e. ( Base ` ( PwSer1 ` R ) ) -> F e. ( Base ` ( 1o mPwSer R ) ) )
12	8 11	syl	|- ( F e. B -> F e. ( Base ` ( 1o mPwSer R ) ) )
13	1 6	ply1bascl	|- ( G e. B -> G e. ( Base ` ( PwSer1 ` R ) ) )
14	9 10	psr1bascl	|- ( G e. ( Base ` ( PwSer1 ` R ) ) -> G e. ( Base ` ( 1o mPwSer R ) ) )
15	13 14	syl	|- ( G e. B -> G e. ( Base ` ( 1o mPwSer R ) ) )
16		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
17		eqid	|- ( 1o mPwSer S ) = ( 1o mPwSer S )
18		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
19	1 18 4	ply1mulr	|- .x. = ( .r ` ( 1o mPoly R ) )
20	18 16 19	mplmulr	|- .x. = ( .r ` ( 1o mPwSer R ) )
21		eqid	|- ( 1o mPoly S ) = ( 1o mPoly S )
22	3 21 5	ply1mulr	|- .xb = ( .r ` ( 1o mPoly S ) )
23	21 17 22	mplmulr	|- .xb = ( .r ` ( 1o mPwSer S ) )
24		eqid	|- ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
25	16 2 17 20 23 24	psropprmul	|- ( ( R e. Ring /\ F e. ( Base ` ( 1o mPwSer R ) ) /\ G e. ( Base ` ( 1o mPwSer R ) ) ) -> ( F .xb G ) = ( G .x. F ) )
26	7 12 15 25	syl3an	|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( G .x. F ) )