Metamath Proof Explorer


Theorem opsr0

Description: Zero in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opsr0.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsr0.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsr0.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsr0 ( 𝜑 → ( 0g𝑆 ) = ( 0g𝑂 ) )

Proof

Step Hyp Ref Expression
1 opsr0.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 opsr0.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3 opsr0.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
4 eqidd ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
5 1 2 3 opsrbas ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑂 ) )
6 1 2 3 opsrplusg ( 𝜑 → ( +g𝑆 ) = ( +g𝑂 ) )
7 6 oveqdr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) = ( 𝑥 ( +g𝑂 ) 𝑦 ) )
8 4 5 7 grpidpropd ( 𝜑 → ( 0g𝑆 ) = ( 0g𝑂 ) )