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

Metamath Proof Explorer

Theorem opsrassa

Description: The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

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

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 psrassa ⊢ φ → I mPwSer R ∈ AssAlg
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 5 2 3 psrsca ⊢ φ → R = Scalar ⁡ I mPwSer R
14 5 1 4 2 3 opsrsca ⊢ φ → R = Scalar ⁡ O
15 eqid ⊢ Base R = Base R
16 5 1 4 opsrvsca ⊢ φ → ⋅ I mPwSer R = ⋅ O
17 16 oveqdr ⊢ φ ∧ x ∈ Base R ∧ y ∈ Base I mPwSer R → x ⋅ I mPwSer R y = x ⋅ O y
18 7 8 10 12 13 14 15 17 assapropd ⊢ φ → I mPwSer R ∈ AssAlg ↔ O ∈ AssAlg
19 6 18 mpbid ⊢ φ → O ∈ AssAlg