Theorem opsr1

Description: One 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	opsr1	|- ( ph -> ( 1r ` S ) = ( 1r ` 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	opsrmulr	|- ( ph -> ( .r ` S ) = ( .r ` O ) )
7	6	oveqdr	|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( .r ` S ) y ) = ( x ( .r ` O ) y ) )
8	4 5 7	rngidpropd	|- ( ph -> ( 1r ` S ) = ( 1r ` O ) )