Metamath Proof Explorer

Theorem resspsrvsca

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

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

Proof

Step Hyp Ref Expression
1 resspsr.s 
 |-  S = ( I mPwSer R )
2 resspsr.h 
 |-  H = ( R |`s T )
3 resspsr.u 
 |-  U = ( I mPwSer H )
4 resspsr.b 
 |-  B = ( Base ` U )
5 resspsr.p 
 |-  P = ( S |`s B )
6 resspsr.2 
 |-  ( ph -> T e. ( SubRing ` R ) )
7 eqid 
 |-  ( .s ` U ) = ( .s ` U )
8 eqid 
 |-  ( Base ` H ) = ( Base ` H )
9 eqid 
 |-  ( .r ` H ) = ( .r ` H )
10 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
11 simprl 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> X e. T )
12 6 adantr 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> T e. ( SubRing ` R ) )
13 2 subrgbas 
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
14 12 13 syl 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> T = ( Base ` H ) )
15 11 14 eleqtrd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> X e. ( Base ` H ) )
16 simprr 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> Y e. B )
17 3 7 8 4 9 10 15 16 psrvsca 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` H ) Y ) )
18 eqid 
 |-  ( .s ` S ) = ( .s ` S )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 eqid 
 |-  ( .r ` R ) = ( .r ` R )
22 19 subrgss 
 |-  ( T e. ( SubRing ` R ) -> T C_ ( Base ` R ) )
23 12 22 syl 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> T C_ ( Base ` R ) )
24 23 11 sseldd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> X e. ( Base ` R ) )
25 1 2 3 4 5 6 resspsrbas 
 |-  ( ph -> B = ( Base ` P ) )
26 5 20 ressbasss 
 |-  ( Base ` P ) C_ ( Base ` S )
27 25 26 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` S ) )
28 27 adantr 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> B C_ ( Base ` S ) )
29 28 16 sseldd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> Y e. ( Base ` S ) )
30 1 18 19 20 21 10 24 29 psrvsca 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` S ) Y ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) Y ) )
31 2 21 ressmulr 
 |-  ( T e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` H ) )
32 ofeq 
 |-  ( ( .r ` R ) = ( .r ` H ) -> oF ( .r ` R ) = oF ( .r ` H ) )
33 12 31 32 3syl 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> oF ( .r ` R ) = oF ( .r ` H ) )
34 33 oveqd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) Y ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` H ) Y ) )
35 30 34 eqtrd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` S ) Y ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` H ) Y ) )
36 4 fvexi 
 |-  B e. _V
37 5 18 ressvsca 
 |-  ( B e. _V -> ( .s ` S ) = ( .s ` P ) )
38 36 37 mp1i 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( .s ` S ) = ( .s ` P ) )
39 38 oveqd 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` S ) Y ) = ( X ( .s ` P ) Y ) )
40 17 35 39 3eqtr2d 
 |-  ( ( ph /\ ( X e. T /\ Y e. B ) ) -> ( X ( .s ` U ) Y ) = ( X ( .s ` P ) Y ) )