Theorem psrcrng

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

	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	psrcrng	$$⊢\phi \to S\in \mathrm{CRing}$$

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		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
5	3 4	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
6	1 2 5	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
7		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
8		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
9	7 8	mgpbas	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
10	9	a1i	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
11		eqid	$$⊢{\cdot }_S={\cdot }_S$$
12	7 11	mgpplusg	$$⊢{\cdot }_S={+}_{{\mathrm{mulGrp}}_S}$$
13	12	a1i	$$⊢\phi \to {\cdot }_S={+}_{{\mathrm{mulGrp}}_S}$$
14	7	ringmgp	$$⊢S\in \mathrm{Ring}\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
15	6 14	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
16	2	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to I\in V$$
17	5	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
18		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\}$$
19		simp2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
20		simp3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to y\in {\mathrm{Base}}_S$$
21	3	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to R\in \mathrm{CRing}$$
22	1 16 17 18 11 8 19 20 21	psrcom	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{\cdot }_{S}y=y{\cdot }_{S}x$$
23	10 13 15 22	iscmnd	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
24	7	iscrng	$$⊢S\in \mathrm{CRing}\leftrightarrow \left(S\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_S\in \mathrm{CMnd}\right)$$
25	6 23 24	sylanbrc	$$⊢\phi \to S\in \mathrm{CRing}$$