Metamath Proof Explorer


Theorem ressmplvsca

Description: A restricted power series algebra has the same scalar 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 ressmplvsca
|- ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` 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
 |-  ( Y e. B -> Y e. ( Base ` ( I mPwSer H ) ) )
12 eqid
 |-  ( I mPwSer R ) = ( I mPwSer R )
13 eqid
 |-  ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) = ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) )
14 12 2 8 9 13 6 resspsrvsca
 |-  ( ( ph /\ ( X e. T /\ Y e. ( Base ` ( I mPwSer H ) ) ) ) -> ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) )
15 11 14 sylanr2
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) )
16 4 fvexi
 |-  B e. _V
17 3 8 4 mplval2
 |-  U = ( ( I mPwSer H ) |`s B )
18 eqid
 |-  ( .s ` ( I mPwSer H ) ) = ( .s ` ( I mPwSer H ) )
19 17 18 ressvsca
 |-  ( B e. _V -> ( .s ` ( I mPwSer H ) ) = ( .s ` U ) )
20 16 19 ax-mp
 |-  ( .s ` ( I mPwSer H ) ) = ( .s ` U )
21 20 oveqi
 |-  ( X ( .s ` ( I mPwSer H ) ) Y ) = ( X ( .s ` U ) Y )
22 fvex
 |-  ( Base ` S ) e. _V
23 eqid
 |-  ( Base ` S ) = ( Base ` S )
24 1 12 23 mplval2
 |-  S = ( ( I mPwSer R ) |`s ( Base ` S ) )
25 eqid
 |-  ( .s ` ( I mPwSer R ) ) = ( .s ` ( I mPwSer R ) )
26 24 25 ressvsca
 |-  ( ( Base ` S ) e. _V -> ( .s ` ( I mPwSer R ) ) = ( .s ` S ) )
27 22 26 ax-mp
 |-  ( .s ` ( I mPwSer R ) ) = ( .s ` S )
28 fvex
 |-  ( Base ` ( I mPwSer H ) ) e. _V
29 13 25 ressvsca
 |-  ( ( Base ` ( I mPwSer H ) ) e. _V -> ( .s ` ( I mPwSer R ) ) = ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) )
30 28 29 ax-mp
 |-  ( .s ` ( I mPwSer R ) ) = ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) )
31 eqid
 |-  ( .s ` S ) = ( .s ` S )
32 7 31 ressvsca
 |-  ( B e. _V -> ( .s ` S ) = ( .s ` P ) )
33 16 32 ax-mp
 |-  ( .s ` S ) = ( .s ` P )
34 27 30 33 3eqtr3i
 |-  ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) = ( .s ` P )
35 34 oveqi
 |-  ( X ( .s ` ( ( I mPwSer R ) |`s ( Base ` ( I mPwSer H ) ) ) ) Y ) = ( X ( .s ` P ) Y )
36 15 21 35 3eqtr3g
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) )