Metamath Proof Explorer

Theorem ressply1vsca

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

Ref Expression
Hypotheses ressply1.s 
|- S = ( Poly1 ` R )
ressply1.h 
|- H = ( R |`s T )
ressply1.u 
|- U = ( Poly1 ` H )
ressply1.b 
|- B = ( Base ` U )
ressply1.2 
|- ( ph -> T e. ( SubRing ` R ) )
ressply1.p 
|- P = ( S |`s B )
Assertion ressply1vsca 
|- ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) )

Proof

Step Hyp Ref Expression
1 ressply1.s 
 |-  S = ( Poly1 ` R )
2 ressply1.h 
 |-  H = ( R |`s T )
3 ressply1.u 
 |-  U = ( Poly1 ` H )
4 ressply1.b 
 |-  B = ( Base ` U )
5 ressply1.2 
 |-  ( ph -> T e. ( SubRing ` R ) )
6 ressply1.p 
 |-  P = ( S |`s B )
7 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
8 eqid 
 |-  ( 1o mPoly H ) = ( 1o mPoly H )
9 eqid 
 |-  ( PwSer1 ` H ) = ( PwSer1 ` H )
10 3 9 4 ply1bas 
 |-  B = ( Base ` ( 1o mPoly H ) )
11 1on 
 |-  1o e. On
12 11 a1i 
 |-  ( ph -> 1o e. On )
13 eqid 
 |-  ( ( 1o mPoly R ) |`s B ) = ( ( 1o mPoly R ) |`s B )
14 7 2 8 10 12 5 13 ressmplvsca 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` ( 1o mPoly H ) ) Y ) = ( X ( .s ` ( ( 1o mPoly R ) |`s B ) ) Y ) )
15 eqid 
 |-  ( .s ` U ) = ( .s ` U )
16 3 8 15 ply1vsca 
 |-  ( .s ` U ) = ( .s ` ( 1o mPoly H ) )
17 16 oveqi 
 |-  ( X ( .s ` U ) Y ) = ( X ( .s ` ( 1o mPoly H ) ) Y )
18 eqid 
 |-  ( .s ` S ) = ( .s ` S )
19 1 7 18 ply1vsca 
 |-  ( .s ` S ) = ( .s ` ( 1o mPoly R ) )
20 4 fvexi 
 |-  B e. _V
21 6 18 ressvsca 
 |-  ( B e. _V -> ( .s ` S ) = ( .s ` P ) )
22 20 21 ax-mp 
 |-  ( .s ` S ) = ( .s ` P )
23 eqid 
 |-  ( .s ` ( 1o mPoly R ) ) = ( .s ` ( 1o mPoly R ) )
24 13 23 ressvsca 
 |-  ( B e. _V -> ( .s ` ( 1o mPoly R ) ) = ( .s ` ( ( 1o mPoly R ) |`s B ) ) )
25 20 24 ax-mp 
 |-  ( .s ` ( 1o mPoly R ) ) = ( .s ` ( ( 1o mPoly R ) |`s B ) )
26 19 22 25 3eqtr3i 
 |-  ( .s ` P ) = ( .s ` ( ( 1o mPoly R ) |`s B ) )
27 26 oveqi 
 |-  ( X ( .s ` P ) Y ) = ( X ( .s ` ( ( 1o mPoly R ) |`s B ) ) Y )
28 14 17 27 3eqtr4g 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) )