Theorem psrvscacl

Description: Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrvscacl.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrvscacl.n	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	psrvscacl.k	$$⊢K={\mathrm{Base}}_R$$
	psrvscacl.b	$$⊢B={\mathrm{Base}}_S$$
	psrvscacl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrvscacl.x	$$⊢\phi \to X\in K$$
	psrvscacl.y	$$⊢\phi \to F\in B$$
Assertion	psrvscacl	$$⊢\phi \to X\underset{\dot{}}{·}F\in B$$

Proof

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