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 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 4 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
11 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
12 10 11 syl 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
13 reldmpsr 
 |-  Rel dom mPwSer
14 13 1 2 elbasov 
 |-  ( X e. B -> ( I e. _V /\ R e. _V ) )
15 5 14 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
16 15 simpld 
 |-  ( ph -> I e. _V )
17 7 psrbaglefi 
 |-  ( ( I e. _V /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
18 16 17 sylan 
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
19 4 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
20 1 8 7 2 5 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
21 20 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
22 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
23 breq1 
 |-  ( y = x -> ( y oR <_ k <-> x oR <_ k ) )
24 23 elrab 
 |-  ( x e. { y e. D | y oR <_ k } <-> ( x e. D /\ x oR <_ k ) )
25 22 24 sylib 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( x e. D /\ x oR <_ k ) )
26 25 simpld 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
27 21 26 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
28 1 8 7 2 6 psrelbas 
 |-  ( ph -> Y : D --> ( Base ` R ) )
29 28 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
30 16 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> I e. _V )
31 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
32 7 psrbagf 
 |-  ( ( I e. _V /\ x e. D ) -> x : I --> NN0 )
33 30 26 32 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x : I --> NN0 )
34 25 simprd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x oR <_ k )
35 7 psrbagcon 
 |-  ( ( I e. _V /\ ( k e. D /\ x : I --> NN0 /\ x oR <_ k ) ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) )
36 30 31 33 34 35 syl13anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( k oF - x ) e. D /\ ( k oF - x ) oR <_ k ) )
37 36 simpld 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
38 29 37 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
39 eqid 
 |-  ( .r ` R ) = ( .r ` R )
40 8 39 ringcl 
 |-  ( ( R e. Ring /\ ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
41 19 27 38 40 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
42 41 fmpttd 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) : { y e. D | y oR <_ k } --> ( Base ` R ) )
43 fvexd 
 |-  ( ( ph /\ k e. D ) -> ( 0g ` R ) e. _V )
44 42 18 43 fdmfifsupp 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )
45 8 9 12 18 42 44 gsumcl 
 |-  ( ( 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 ) )
46 45 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 ) )
47 fvex 
 |-  ( Base ` R ) e. _V
48 ovex 
 |-  ( NN0 ^m I ) e. _V
49 7 48 rabex2 
 |-  D e. _V
50 47 49 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 ) )
51 46 50 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 ) )
52 1 2 39 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 ) ) ) ) ) ) )
53 1 8 7 2 16 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m D ) )
54 51 52 53 3eltr4d 
 |-  ( ph -> ( X .x. Y ) e. B )