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=ImPwSerR
opsrbas.o O=IordPwSerRT
opsrbas.t φTI×I
Assertion opsrmulr φS=O

Proof

Step Hyp Ref Expression
1 opsrbas.s S=ImPwSerR
2 opsrbas.o O=IordPwSerRT
3 opsrbas.t φTI×I
4 mulrid 𝑟=Slotndx
5 plendxnmulrndx ndxndx
6 5 necomi ndxndx
7 1 2 3 4 6 opsrbaslem φS=O