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)

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 df-mulr 𝑟 = Slot 3
5 3nn 3
6 3lt10 3 < 10
7 1 2 3 4 5 6 opsrbaslem φ S = O