Metamath Proof Explorer


Theorem opsrmulrOLD

Description: Obsolete version of opsrmulr as of 1-Nov-2024. The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses opsrbas.s S=ImPwSerR
opsrbas.o O=IordPwSerRT
opsrbas.t φTI×I
Assertion opsrmulrOLD φS=O

Proof

Step Hyp Ref Expression
1 opsrbas.s S=ImPwSerR
2 opsrbas.o O=IordPwSerRT
3 opsrbas.t φTI×I
4 df-mulr 𝑟=Slot3
5 3nn 3
6 3lt10 3<10
7 1 2 3 4 5 6 opsrbaslemOLD φS=O