This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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