Metamath Proof Explorer


Theorem opsrring

Description: Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses opsrring.o O=IordPwSerRT
opsrring.i φIV
opsrring.r φRRing
opsrring.t φTI×I
Assertion opsrring φORing

Proof

Step Hyp Ref Expression
1 opsrring.o O=IordPwSerRT
2 opsrring.i φIV
3 opsrring.r φRRing
4 opsrring.t φTI×I
5 eqid ImPwSerR=ImPwSerR
6 5 2 3 psrring φImPwSerRRing
7 eqidd φBaseImPwSerR=BaseImPwSerR
8 5 1 4 opsrbas φBaseImPwSerR=BaseO
9 5 1 4 opsrplusg φ+ImPwSerR=+O
10 9 oveqdr φxBaseImPwSerRyBaseImPwSerRx+ImPwSerRy=x+Oy
11 5 1 4 opsrmulr φImPwSerR=O
12 11 oveqdr φxBaseImPwSerRyBaseImPwSerRxImPwSerRy=xOy
13 7 8 10 12 ringpropd φImPwSerRRingORing
14 6 13 mpbid φORing