Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Univariate polynomials
opsrring
Next ⟩
opsrlmod
Metamath Proof Explorer
Ascii
Unicode
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