Theorem opsrassa

Description: The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

	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	opsrassa	$$⊢\phi \to O\in \mathrm{AssAlg}$$

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	psrassa	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{AssAlg}$$
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	5 2 3	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)$$
14	5 1 4 2 3	opsrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(O\right)$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16	5 1 4	opsrvsca	$$⊢\phi \to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_O$$
17	16	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\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$$
18	7 8 10 12 13 14 15 17	assapropd	$$⊢\phi \to \left(I\mathrm{mPwSer}R\in \mathrm{AssAlg}\leftrightarrow O\in \mathrm{AssAlg}\right)$$
19	6 18	mpbid	$$⊢\phi \to O\in \mathrm{AssAlg}$$