Metamath Proof Explorer


Theorem opsrmulr

Description: The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

Ref Expression
Hypotheses opsrbas.s
|- S = ( I mPwSer R )
opsrbas.o
|- O = ( ( I ordPwSer R ) ` T )
opsrbas.t
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrmulr
|- ( ph -> ( .r ` S ) = ( .r ` O ) )

Proof

Step Hyp Ref Expression
1 opsrbas.s
 |-  S = ( I mPwSer R )
2 opsrbas.o
 |-  O = ( ( I ordPwSer R ) ` T )
3 opsrbas.t
 |-  ( ph -> T C_ ( I X. I ) )
4 mulrid
 |-  .r = Slot ( .r ` ndx )
5 plendxnmulrndx
 |-  ( le ` ndx ) =/= ( .r ` ndx )
6 5 necomi
 |-  ( .r ` ndx ) =/= ( le ` ndx )
7 1 2 3 4 6 opsrbaslem
 |-  ( ph -> ( .r ` S ) = ( .r ` O ) )