Metamath Proof Explorer


Theorem psrmulcllem

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 )
psrmulcl.d
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrmulcllem
|- ( 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 psrmulcl.d
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
8 eqid
 |-  ( Base ` R ) = ( Base ` R )
9 1 8 7 2 5 psrelbas
 |-  ( ph -> X : D --> ( Base ` R ) )
10 1 8 7 2 6 psrelbas
 |-  ( ph -> Y : D --> ( Base ` R ) )
11 7 4 9 10 rhmpsrlem2
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. ( Base ` R ) )
12 11 fmpttd
 |-  ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) : D --> ( Base ` R ) )
13 fvex
 |-  ( Base ` R ) e. _V
14 ovex
 |-  ( NN0 ^m I ) e. _V
15 7 14 rabex2
 |-  D e. _V
16 13 15 elmap
 |-  ( ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) e. ( ( Base ` R ) ^m D ) <-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) : D --> ( Base ` R ) )
17 12 16 sylibr
 |-  ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) e. ( ( Base ` R ) ^m D ) )
18 eqid
 |-  ( .r ` R ) = ( .r ` R )
19 1 2 18 3 7 5 6 psrmulfval
 |-  ( ph -> ( X .x. Y ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
20 reldmpsr
 |-  Rel dom mPwSer
21 20 1 2 elbasov
 |-  ( X e. B -> ( I e. _V /\ R e. _V ) )
22 5 21 syl
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
23 22 simpld
 |-  ( ph -> I e. _V )
24 1 8 7 2 23 psrbas
 |-  ( ph -> B = ( ( Base ` R ) ^m D ) )
25 17 19 24 3eltr4d
 |-  ( ph -> ( X .x. Y ) e. B )