Metamath Proof Explorer


Theorem opsrring

Description: Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 opsrring.o
 |-  O = ( ( I ordPwSer R ) ` T )
2 opsrring.i
 |-  ( ph -> I e. V )
3 opsrring.r
 |-  ( ph -> R e. Ring )
4 opsrring.t
 |-  ( ph -> T C_ ( I X. I ) )
5 eqid
 |-  ( I mPwSer R ) = ( I mPwSer R )
6 5 2 3 psrring
 |-  ( ph -> ( I mPwSer R ) e. Ring )
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 7 8 10 12 ringpropd
 |-  ( ph -> ( ( I mPwSer R ) e. Ring <-> O e. Ring ) )
14 6 13 mpbid
 |-  ( ph -> O e. Ring )