Theorem opsrring

Description: Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypotheses	opsrring.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsrring.i	$$⊢\phi \to I\in V$$
	opsrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	opsrring.t	$$⊢\phi \to T\subseteq I\times I$$
Assertion	opsrring	$$⊢\phi \to O\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		opsrring.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
2		opsrring.i	$$⊢\phi \to I\in V$$
3		opsrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		opsrring.t	$$⊢\phi \to T\subseteq I\times I$$
5		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
6	5 2 3	psrring	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{Ring}$$
7		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8	5 1 4	opsrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_O$$
9	5 1 4	opsrplusg	$$⊢\phi \to {+}_{\left(I\mathrm{mPwSer}R\right)}={+}_O$$
10	9	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\right)\to x{+}_{\left(I\mathrm{mPwSer}R\right)}y=x{+}_{O}y$$
11	5 1 4	opsrmulr	$$⊢\phi \to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_O$$
12	11	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\right)\to x{\cdot }_{\left(I\mathrm{mPwSer}R\right)}y=x{\cdot }_{O}y$$
13	7 8 10 12	ringpropd	$$⊢\phi \to \left(I\mathrm{mPwSer}R\in \mathrm{Ring}\leftrightarrow O\in \mathrm{Ring}\right)$$
14	6 13	mpbid	$$⊢\phi \to O\in \mathrm{Ring}$$