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 mPwSer R )
	psrvscacl.n	|- .x. = ( .s ` S )
	psrvscacl.k	|- K = ( Base ` R )
	psrvscacl.b	|- B = ( Base ` S )
	psrvscacl.r	|- ( ph -> R e. Ring )
	psrvscacl.x	|- ( ph -> X e. K )
	psrvscacl.y	|- ( ph -> F e. B )
Assertion	psrvscacl	|- ( ph -> ( X .x. F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		psrvscacl.s	|- S = ( I mPwSer R )
2		psrvscacl.n	|- .x. = ( .s ` S )
3		psrvscacl.k	|- K = ( Base ` R )
4		psrvscacl.b	|- B = ( Base ` S )
5		psrvscacl.r	|- ( ph -> R e. Ring )
6		psrvscacl.x	|- ( ph -> X e. K )
7		psrvscacl.y	|- ( ph -> F e. B )
8		eqid	|- ( .r ` R ) = ( .r ` R )
9	3 8	ringcl	|- ( ( R e. Ring /\ x e. K /\ y e. K ) -> ( x ( .r ` R ) y ) e. K )
10	9	3expb	|- ( ( R e. Ring /\ ( x e. K /\ y e. K ) ) -> ( x ( .r ` R ) y ) e. K )
11	5 10	sylan	|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( .r ` R ) y ) e. K )
12		fconst6g	|- ( X e. K -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> K )
13	6 12	syl	|- ( ph -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> K )
14		eqid	|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15	1 3 14 4 7	psrelbas	|- ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> K )
16		ovex	|- ( NN0 ^m I ) e. _V
17	16	rabex	|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
18	17	a1i	|- ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
19		inidm	|- ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } i^i { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
20	11 13 15 18 18 19	off	|- ( ph -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> K )
21	3	fvexi	|- K e. _V
22	21 17	elmap	|- ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) F ) e. ( K ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> K )
23	20 22	sylibr	|- ( ph -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) F ) e. ( K ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
24	1 2 3 4 8 14 6 7	psrvsca	|- ( ph -> ( X .x. F ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { X } ) oF ( .r ` R ) F ) )
25		reldmpsr	|- Rel dom mPwSer
26	25 1 4	elbasov	|- ( F e. B -> ( I e. _V /\ R e. _V ) )
27	7 26	syl	|- ( ph -> ( I e. _V /\ R e. _V ) )
28	27	simpld	|- ( ph -> I e. _V )
29	1 3 14 4 28	psrbas	|- ( ph -> B = ( K ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
30	23 24 29	3eltr4d	|- ( ph -> ( X .x. F ) e. B )