Theorem opsrcrng

Description: The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		opsrcrng.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
2		opsrcrng.i	$$⊢\phi \to I\in V$$
3		opsrcrng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		opsrcrng.t	$$⊢\phi \to T\subseteq I\times I$$
5		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
6	5 2 3	psrcrng	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{CRing}$$
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	crngpropd	$$⊢\phi \to \left(I\mathrm{mPwSer}R\in \mathrm{CRing}\leftrightarrow O\in \mathrm{CRing}\right)$$
14	6 13	mpbid	$$⊢\phi \to O\in \mathrm{CRing}$$