# 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$