This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )