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	3	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
8	1 2 7	psrgrp	$$⊢\phi \to S\in \mathrm{Grp}$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10		eqid	$$⊢{\cdot }_S={\cdot }_S$$
11	3	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
12		simp2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
13		simp3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to y\in {\mathrm{Base}}_S$$
14	1 9 10 11 12 13	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$$
15	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$$
16	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}$$
17		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\}$$
18		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$$
19		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$$
20		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$$
21	1 15 16 17 10 9 18 19 20	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)$$
22		eqid	$$⊢{+}_S={+}_S$$
23	1 15 16 17 10 9 18 19 20 22	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)$$
24	1 15 16 17 10 9 18 19 20 22	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)$$
25		eqid	$$⊢0_R=0_R$$
26		eqid	$$⊢1_R=1_R$$
27		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)$$
28	1 2 3 17 25 26 27 9	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$$
29	2	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to I\in V$$
30	3	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
31		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
32	1 29 30 17 25 26 27 9 10 31	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$$
33	1 29 30 17 25 26 27 9 10 31	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$$
34	4 5 6 8 14 21 23 24 28 32 33	isringd	$$⊢\phi \to S\in \mathrm{Ring}$$