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

Metamath Proof Explorer

Theorem opsrcrng

Description: The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses opsrcrng.o ⊢ O = I ordPwSer R ⁡ T
opsrcrng.i ⊢ φ → I ∈ V
opsrcrng.r ⊢ φ → R ∈ CRing
opsrcrng.t ⊢ φ → T ⊆ I × I
Assertion opsrcrng ⊢ φ → O ∈ CRing

Proof

Step Hyp Ref Expression
1 opsrcrng.o ⊢ O = I ordPwSer R ⁡ T
2 opsrcrng.i ⊢ φ → I ∈ V
3 opsrcrng.r ⊢ φ → R ∈ CRing
4 opsrcrng.t ⊢ φ → T ⊆ I × I
5 eqid ⊢ I mPwSer R = I mPwSer R
6 5 2 3 psrcrng ⊢ φ → I mPwSer R ∈ CRing
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 crngpropd ⊢ φ → I mPwSer R ∈ CRing ↔ O ∈ CRing
14 6 13 mpbid ⊢ φ → O ∈ CRing