Theorem psrmulcllem

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

	Ref	Expression
Hypotheses	psrmulcl.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrmulcl.b	$$⊢B={\mathrm{Base}}_S$$
	psrmulcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	psrmulcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrmulcl.x	$$⊢\phi \to X\in B$$
	psrmulcl.y	$$⊢\phi \to Y\in B$$
	psrmulcl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	psrmulcllem	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		psrmulcl.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrmulcl.b	$$⊢B={\mathrm{Base}}_S$$
3		psrmulcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
4		psrmulcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		psrmulcl.x	$$⊢\phi \to X\in B$$
6		psrmulcl.y	$$⊢\phi \to Y\in B$$
7		psrmulcl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	1 8 7 2 5	psrelbas	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
10	1 8 7 2 6	psrelbas	$$⊢\phi \to Y:D⟶{\mathrm{Base}}_R$$
11	7 4 9 10	rhmpsrlem2	$$⊢\left(\phi \wedge k\in D\right)\to \underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\in {\mathrm{Base}}_R$$
12	11	fmpttd	$$⊢\phi \to \left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\right):D⟶{\mathrm{Base}}_R$$
13		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
14		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
15	7 14	rabex2	$$⊢D\in \mathrm{V}$$
16	13 15	elmap	$$⊢\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\right):D⟶{\mathrm{Base}}_R$$
17	12 16	sylibr	$$⊢\phi \to \left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)$$
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	1 2 18 3 7 5 6	psrmulfval	$$⊢\phi \to X\underset{\dot{}}{·}Y=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(X\left(x\right){\cdot }_{R}Y\left(k{-}_{f}x\right)\right)\right)$$
20		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
21	20 1 2	elbasov	$$⊢X\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
22	5 21	syl	$$⊢\phi \to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
23	22	simpld	$$⊢\phi \to I\in \mathrm{V}$$
24	1 8 7 2 23	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^D$$
25	17 19 24	3eltr4d	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$