Theorem psrmulcl

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$$
Assertion	psrmulcl	$$⊢\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		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\}$$
8	1 2 3 4 5 6 7	psrmulcllem	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$