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

Metamath Proof Explorer

Theorem opsrlmod

Description: Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-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 opsrlmod ⊢ φ → O ∈ LMod

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