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\mathrm{mPwSer}R$$
	opsr0.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsr0.t	$$⊢\phi \to T\subseteq I\times I$$
Assertion	opsr1	$$⊢\phi \to 1_S=1_O$$

Proof

Step	Hyp	Ref	Expression
1		opsr0.s	$$⊢S=I\mathrm{mPwSer}R$$
2		opsr0.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
3		opsr0.t	$$⊢\phi \to T\subseteq I\times I$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
5	1 2 3	opsrbas	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_O$$
6	1 2 3	opsrmulr	$$⊢\phi \to {\cdot }_S={\cdot }_O$$
7	6	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x{\cdot }_{S}y=x{\cdot }_{O}y$$
8	4 5 7	rngidpropd	$$⊢\phi \to 1_S=1_O$$