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 = I ordPwSer R T
opsrring.i φ I V
opsrring.r φ R Ring
opsrring.t φ T I × I
Assertion opsrring φ O Ring

Proof

Step Hyp Ref Expression
1 opsrring.o O = I ordPwSer R T
2 opsrring.i φ I V
3 opsrring.r φ R Ring
4 opsrring.t φ T I × I
5 eqid I mPwSer R = I mPwSer R
6 5 2 3 psrring φ I mPwSer R Ring
7 eqidd φ Base I mPwSer R = Base I mPwSer R
8 5 1 4 opsrbas φ Base I mPwSer R = Base O
9 5 1 4 opsrplusg φ + I mPwSer R = + O
10 9 oveqdr φ x Base I mPwSer R y Base I mPwSer R x + I mPwSer R y = x + O y
11 5 1 4 opsrmulr φ I mPwSer R = O
12 11 oveqdr φ x Base I mPwSer R y Base I mPwSer R x I mPwSer R y = x O y
13 7 8 10 12 ringpropd φ I mPwSer R Ring O Ring
14 6 13 mpbid φ O Ring