Metamath Proof Explorer


Theorem opsrplusgOLD

Description: Obsolete version of opsrplusg as of 1-Nov-2024. The addition 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 opsrplusgOLD φ+S=+O

Proof

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