Theorem psrmulcl

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

	Ref	Expression
Hypotheses	psrmulcl.s	|- S = ( I mPwSer R )
	psrmulcl.b	|- B = ( Base ` S )
	psrmulcl.t	|- .x. = ( .r ` S )
	psrmulcl.r	|- ( ph -> R e. Ring )
	psrmulcl.x	|- ( ph -> X e. B )
	psrmulcl.y	|- ( ph -> Y e. B )
Assertion	psrmulcl	|- ( ph -> ( X .x. Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		psrmulcl.s	|- S = ( I mPwSer R )
2		psrmulcl.b	|- B = ( Base ` S )
3		psrmulcl.t	|- .x. = ( .r ` S )
4		psrmulcl.r	|- ( ph -> R e. Ring )
5		psrmulcl.x	|- ( ph -> X e. B )
6		psrmulcl.y	|- ( ph -> Y e. B )
7		eqid	|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
8	1 2 3 4 5 6 7	psrmulcllem	|- ( ph -> ( X .x. Y ) e. B )