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 ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrcrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrcrng.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
opsrcrng.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsrassa ( 𝜑 → 𝑂 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 opsrcrng.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrcrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 opsrcrng.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 opsrcrng.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6 5 2 3 psrassa ⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg )
7 eqidd ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
8 5 1 4 opsrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ 𝑂 ) )
9 5 1 4 opsrplusg ⊢ ( 𝜑 → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑂 ) )
10 9 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
11 5 1 4 opsrmulr ⊢ ( 𝜑 → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑂 ) )
12 11 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) )
13 5 2 3 psrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) )
14 5 1 4 2 3 opsrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 5 1 4 opsrvsca ⊢ ( 𝜑 → ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠 ‘ 𝑂 ) )
17 16 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) 𝑦 ) )
18 7 8 10 12 13 14 15 17 assapropd ⊢ ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg ↔ 𝑂 ∈ AssAlg ) )
19 6 18 mpbid ⊢ ( 𝜑 → 𝑂 ∈ AssAlg )