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	3	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
10	1 2 9	psrlmod	$$⊢\phi \to S\in \mathrm{LMod}$$
11	1 2 9	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
12	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$$
13	9	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}$$
14		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\}$$
15		eqid	$$⊢{\cdot }_S={\cdot }_S$$
16		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
17		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$$
18		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$$
19	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}$$
20		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
21		eqid	$$⊢{\cdot }_S={\cdot }_S$$
22		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$$
23	1 12 13 14 15 16 17 18 19 20 21 22	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)$$
24	23	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)$$
25	23	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)$$
26	4 5 6 7 8 10 11 24 25	isassad	$$⊢\phi \to S\in \mathrm{AssAlg}$$