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 φ T I × I
Assertion opsrmulr φ S = O

Proof

Step Hyp Ref Expression
1 opsrbas.s S = I mPwSer R
2 opsrbas.o O = I ordPwSer R T
3 opsrbas.t φ T I × I
4 mulrid 𝑟 = Slot ndx
5 plendxnmulrndx ndx ndx
6 5 necomi ndx ndx
7 1 2 3 4 6 opsrbaslem φ S = O