Metamath Proof Explorer

Theorem opsrassa

Description: The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses opsrcrng.o 
|- O = ( ( I ordPwSer R ) ` T )
opsrcrng.i 
|- ( ph -> I e. V )
opsrcrng.r 
|- ( ph -> R e. CRing )
opsrcrng.t 
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrassa 
|- ( ph -> O e. AssAlg )

Proof

Step Hyp Ref Expression
1 opsrcrng.o 
 |-  O = ( ( I ordPwSer R ) ` T )
2 opsrcrng.i 
 |-  ( ph -> I e. V )
3 opsrcrng.r 
 |-  ( ph -> R e. CRing )
4 opsrcrng.t 
 |-  ( ph -> T C_ ( I X. I ) )
5 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
6 5 2 3 psrassa 
 |-  ( ph -> ( I mPwSer R ) e. AssAlg )
7 eqidd 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) )
8 5 1 4 opsrbas 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` O ) )
9 5 1 4 opsrplusg 
 |-  ( ph -> ( +g ` ( I mPwSer R ) ) = ( +g ` O ) )
10 9 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( +g ` ( I mPwSer R ) ) y ) = ( x ( +g ` O ) y ) )
11 5 1 4 opsrmulr 
 |-  ( ph -> ( .r ` ( I mPwSer R ) ) = ( .r ` O ) )
12 11 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( .r ` ( I mPwSer R ) ) y ) = ( x ( .r ` O ) y ) )
13 5 2 3 psrsca 
 |-  ( ph -> R = ( Scalar ` ( I mPwSer R ) ) )
14 5 1 4 2 3 opsrsca 
 |-  ( ph -> R = ( Scalar ` O ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 5 1 4 opsrvsca 
 |-  ( ph -> ( .s ` ( I mPwSer R ) ) = ( .s ` O ) )
17 16 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( .s ` ( I mPwSer R ) ) y ) = ( x ( .s ` O ) y ) )
18 7 8 10 12 13 14 15 17 assapropd 
 |-  ( ph -> ( ( I mPwSer R ) e. AssAlg <-> O e. AssAlg ) )
19 6 18 mpbid 
 |-  ( ph -> O e. AssAlg )