Theorem opsrlmod

Description: Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-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	opsrlmod	$$⊢\phi \to O\in \mathrm{LMod}$$

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