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 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrring.i ( 𝜑𝐼𝑉 )
opsrring.r ( 𝜑𝑅 ∈ Ring )
opsrring.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsrring ( 𝜑𝑂 ∈ Ring )

Proof

Step Hyp Ref Expression
1 opsrring.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrring.i ( 𝜑𝐼𝑉 )
3 opsrring.r ( 𝜑𝑅 ∈ Ring )
4 opsrring.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6 5 2 3 psrring ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ Ring )
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 7 8 10 12 ringpropd ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) ∈ Ring ↔ 𝑂 ∈ Ring ) )
14 6 13 mpbid ( 𝜑𝑂 ∈ Ring )