This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )