Theorem psrring

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

	Ref	Expression
Hypotheses	psrring.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrring.i	$$⊢\phi \to I\in V$$
	psrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrring.i	$$⊢\phi \to I\in V$$
3		psrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
5		eqidd	$$⊢\phi \to {+}_S={+}_S$$
6		eqidd	$$⊢\phi \to {\cdot }_S={\cdot }_S$$
7		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
8	3 7	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
9	1 2 8	psrgrp	$$⊢\phi \to S\in \mathrm{Grp}$$
10		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
11		eqid	$$⊢{\cdot }_S={\cdot }_S$$
12	3	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
13		simp2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
14		simp3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to y\in {\mathrm{Base}}_S$$
15	1 10 11 12 13 14	psrmulcl	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{\cdot }_{S}y\in {\mathrm{Base}}_S$$
16	2	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to I\in V$$
17	3	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\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		simpr1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to x\in {\mathrm{Base}}_S$$
20		simpr2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to y\in {\mathrm{Base}}_S$$
21		simpr3	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to z\in {\mathrm{Base}}_S$$
22	1 16 17 18 11 10 19 20 21	psrass1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\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)$$
23		eqid	$$⊢{+}_S={+}_S$$
24	1 16 17 18 11 10 19 20 21 23	psrdi	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to x{\cdot }_S\left(y{+}_{S}z\right)=\left(x{\cdot }_{S}y\right){+}_S\left(x{\cdot }_{S}z\right)$$
25	1 16 17 18 11 10 19 20 21 23	psrdir	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\right)\to \left(x{+}_{S}y\right){\cdot }_{S}z=\left(x{\cdot }_{S}z\right){+}_S\left(y{\cdot }_{S}z\right)$$
26		eqid	$$⊢0_R=0_R$$
27		eqid	$$⊢1_R=1_R$$
28		eqid	$$⊢\left(r\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(r=I\times \left\{0\right\},1_R,0_R\right)\right)=\left(r\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(r=I\times \left\{0\right\},1_R,0_R\right)\right)$$
29	1 2 3 18 26 27 28 10	psr1cl	$$⊢\phi \to \left(r\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(r=I\times \left\{0\right\},1_R,0_R\right)\right)\in {\mathrm{Base}}_S$$
30	2	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to I\in V$$
31	3	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
32		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
33	1 30 31 18 26 27 28 10 11 32	psrlidm	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to \left(r\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(r=I\times \left\{0\right\},1_R,0_R\right)\right){\cdot }_{S}x=x$$
34	1 30 31 18 26 27 28 10 11 32	psrridm	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to x{\cdot }_S\left(r\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(r=I\times \left\{0\right\},1_R,0_R\right)\right)=x$$
35	4 5 6 9 15 22 24 25 29 33 34	isringd	$$⊢\phi \to S\in \mathrm{Ring}$$