Metamath Proof Explorer


Theorem opsr1

Description: One in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opsr0.s S=ImPwSerR
opsr0.o O=IordPwSerRT
opsr0.t φTI×I
Assertion opsr1 φ1S=1O

Proof

Step Hyp Ref Expression
1 opsr0.s S=ImPwSerR
2 opsr0.o O=IordPwSerRT
3 opsr0.t φTI×I
4 eqidd φBaseS=BaseS
5 1 2 3 opsrbas φBaseS=BaseO
6 1 2 3 opsrmulr φS=O
7 6 oveqdr φxBaseSyBaseSxSy=xOy
8 4 5 7 rngidpropd φ1S=1O