Theorem psraddcl

Description: Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	psraddcl.s	$$⊢S=I\mathrm{mPwSer}R$$
	psraddcl.b	$$⊢B={\mathrm{Base}}_S$$
	psraddcl.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	psraddcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	psraddcl.x	$$⊢\phi \to X\in B$$
	psraddcl.y	$$⊢\phi \to Y\in B$$
Assertion	psraddcl	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		psraddcl.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psraddcl.b	$$⊢B={\mathrm{Base}}_S$$
3		psraddcl.p	$$⊢\underset{\dot{}}{+}={+}_S$$
4		psraddcl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		psraddcl.x	$$⊢\phi \to X\in B$$
6		psraddcl.y	$$⊢\phi \to Y\in B$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢{+}_R={+}_R$$
9	7 8	grpcl	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\to x{+}_{R}y\in {\mathrm{Base}}_R$$
10	9	3expb	$$⊢\left(R\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{R}y\in {\mathrm{Base}}_R$$
11	4 10	sylan	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{R}y\in {\mathrm{Base}}_R$$
12		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\}$$
13	1 7 12 2 5	psrelbas	$$⊢\phi \to X:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
14	1 7 12 2 6	psrelbas	$$⊢\phi \to Y:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
15		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
16	15	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
18		inidm	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\cap \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	11 13 14 17 17 18	off	$$⊢\phi \to \left(X{{+}_R}_{f}Y\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
20		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
21	20 16	elmap	$$⊢X{{+}_R}_{f}Y\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\leftrightarrow \left(X{{+}_R}_{f}Y\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
22	19 21	sylibr	$$⊢\phi \to X{{+}_R}_{f}Y\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
23	1 2 8 3 5 6	psradd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X{{+}_R}_{f}Y$$
24		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
25	24 1 2	elbasov	$$⊢X\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
26	5 25	syl	$$⊢\phi \to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
27	26	simpld	$$⊢\phi \to I\in \mathrm{V}$$
28	1 7 12 2 27	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
29	22 23 28	3eltr4d	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$