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	|- S = ( I mPwSer R )
	opsr0.o	|- O = ( ( I ordPwSer R ) ` T )
	opsr0.t	|- ( ph -> T C_ ( I X. I ) )
Assertion	opsr0	|- ( ph -> ( 0g ` S ) = ( 0g ` O ) )

Proof

Step	Hyp	Ref	Expression
1		opsr0.s	|- S = ( I mPwSer R )
2		opsr0.o	|- O = ( ( I ordPwSer R ) ` T )
3		opsr0.t	|- ( ph -> T C_ ( I X. I ) )
4		eqidd	|- ( ph -> ( Base ` S ) = ( Base ` S ) )
5	1 2 3	opsrbas	|- ( ph -> ( Base ` S ) = ( Base ` O ) )
6	1 2 3	opsrplusg	|- ( ph -> ( +g ` S ) = ( +g ` O ) )
7	6	oveqdr	|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) = ( x ( +g ` O ) y ) )
8	4 5 7	grpidpropd	|- ( ph -> ( 0g ` S ) = ( 0g ` O ) )