Metamath Proof Explorer

Theorem ressmplmul

Description: A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressmpl.s 
|- S = ( I mPoly R )
ressmpl.h 
|- H = ( R |`s T )
ressmpl.u 
|- U = ( I mPoly H )
ressmpl.b 
|- B = ( Base ` U )
ressmpl.1 
|- ( ph -> I e. V )
ressmpl.2 
|- ( ph -> T e. ( SubRing ` R ) )
ressmpl.p 
|- P = ( S |`s B )
Assertion ressmplmul 
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )

Proof

Step Hyp Ref Expression
1 ressmpl.s 
 |-  S = ( I mPoly R )
2 ressmpl.h 
 |-  H = ( R |`s T )
3 ressmpl.u 
 |-  U = ( I mPoly H )
4 ressmpl.b 
 |-  B = ( Base ` U )
5 ressmpl.1 
 |-  ( ph -> I e. V )
6 ressmpl.2 
 |-  ( ph -> T e. ( SubRing ` R ) )
7 ressmpl.p 
 |-  P = ( S |`s B )
8 eqid 
 |-  ( I mPwSer H ) = ( I mPwSer H )
9 eqid 
 |-  ( Base ` ( I mPwSer H ) ) = ( Base ` ( I mPwSer H ) )
10 3 8 4 9 mplbasss 
 |-  B C_ ( Base ` ( I mPwSer H ) )
11 10 sseli 
 |-  ( X e. B -> X e. ( Base ` ( I mPwSer H ) ) )
12 10 sseli 
 |-  ( Y e. B -> Y e. ( Base ` ( I mPwSer H ) ) )
13 11 12 anim12i 
 |-  ( ( X e. B /\ Y e. B ) -> ( X e. ( Base ` ( I mPwSer H ) ) /\ Y e. ( Base ` ( I mPwSer H ) ) ) )
14 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
15 eqid 
 |-  ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) = ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) )
16 14 2 8 9 15 6 resspsrmul 
 |-  ( ( ph /\ ( X e. ( Base ` ( I mPwSer H ) ) /\ Y e. ( Base ` ( I mPwSer H ) ) ) ) -> ( X ( .r ` ( I mPwSer H ) ) Y ) = ( X ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) )
17 13 16 sylan2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` ( I mPwSer H ) ) Y ) = ( X ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) )
18 4 fvexi 
 |-  B e. _V
19 3 8 4 mplval2 
 |-  U = ( ( I mPwSer H ) |`s B )
20 eqid 
 |-  ( .r ` ( I mPwSer H ) ) = ( .r ` ( I mPwSer H ) )
21 19 20 ressmulr 
 |-  ( B e. _V -> ( .r ` ( I mPwSer H ) ) = ( .r ` U ) )
22 18 21 ax-mp 
 |-  ( .r ` ( I mPwSer H ) ) = ( .r ` U )
23 22 oveqi 
 |-  ( X ( .r ` ( I mPwSer H ) ) Y ) = ( X ( .r ` U ) Y )
24 fvex 
 |-  ( Base ` S ) e. _V
25 eqid 
 |-  ( Base ` S ) = ( Base ` S )
26 1 14 25 mplval2 
 |-  S = ( ( I mPwSer R ) |`s ( Base ` S ) )
27 eqid 
 |-  ( .r ` ( I mPwSer R ) ) = ( .r ` ( I mPwSer R ) )
28 26 27 ressmulr 
 |-  ( ( Base ` S ) e. _V -> ( .r ` ( I mPwSer R ) ) = ( .r ` S ) )
29 24 28 ax-mp 
 |-  ( .r ` ( I mPwSer R ) ) = ( .r ` S )
30 fvex 
 |-  ( Base ` ( I mPwSer H ) ) e. _V
31 15 27 ressmulr 
 |-  ( ( Base ` ( I mPwSer H ) ) e. _V -> ( .r ` ( I mPwSer R ) ) = ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) )
32 30 31 ax-mp 
 |-  ( .r ` ( I mPwSer R ) ) = ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) )
33 eqid 
 |-  ( .r ` S ) = ( .r ` S )
34 7 33 ressmulr 
 |-  ( B e. _V -> ( .r ` S ) = ( .r ` P ) )
35 18 34 ax-mp 
 |-  ( .r ` S ) = ( .r ` P )
36 29 32 35 3eqtr3i 
 |-  ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) = ( .r ` P )
37 36 oveqi 
 |-  ( X ( .r ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) = ( X ( .r ` P ) Y )
38 17 23 37 3eqtr3g 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )