Theorem psrassa

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

	Ref	Expression
Hypotheses	psrcnrg.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrcnrg.i	$$⊢\phi \to I\in V$$
	psrcnrg.r	$$⊢\phi \to R\in \mathrm{CRing}$$
Assertion	psrassa	$$⊢\phi \to S\in \mathrm{AssAlg}$$

Proof

Step	Hyp	Ref	Expression
1		psrcnrg.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrcnrg.i	$$⊢\phi \to I\in V$$
3		psrcnrg.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
5	1 2 3	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$
6		eqidd	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
7		eqidd	$$⊢\phi \to {\cdot }_S={\cdot }_S$$
8		eqidd	$$⊢\phi \to {\cdot }_S={\cdot }_S$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10	3 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
11	1 2 10	psrlmod	$$⊢\phi \to S\in \mathrm{LMod}$$
12	1 2 10	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
13	2	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to I\in V$$
14	10	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to R\in \mathrm{Ring}$$
15		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
16		eqid	$$⊢{\cdot }_S={\cdot }_S$$
17		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
18		simpr2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to y\in {\mathrm{Base}}_S$$
19		simpr3	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to z\in {\mathrm{Base}}_S$$
20	3	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to R\in \mathrm{CRing}$$
21		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
22		eqid	$$⊢{\cdot }_S={\cdot }_S$$
23		simpr1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to x\in {\mathrm{Base}}_R$$
24	1 13 14 15 16 17 18 19 20 21 22 23	psrass23	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to \left(\left(x{\cdot }_{S}y\right){\cdot }_{S}z=x{\cdot }_S\left(y{\cdot }_{S}z\right)\wedge y{\cdot }_S\left(x{\cdot }_{S}z\right)=x{\cdot }_S\left(y{\cdot }_{S}z\right)\right)$$
25	24	simpld	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to \left(x{\cdot }_{S}y\right){\cdot }_{S}z=x{\cdot }_S\left(y{\cdot }_{S}z\right)$$
26	24	simprd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to y{\cdot }_S\left(x{\cdot }_{S}z\right)=x{\cdot }_S\left(y{\cdot }_{S}z\right)$$
27	4 5 6 7 8 11 12 3 25 26	isassad	$$⊢\phi \to S\in \mathrm{AssAlg}$$