Metamath Proof Explorer

Theorem psrmulr

Description: The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses psrmulr.s 
|- S = ( I mPwSer R )
psrmulr.b 
|- B = ( Base ` S )
psrmulr.m 
|- .x. = ( .r ` R )
psrmulr.t 
|- .xb = ( .r ` S )
psrmulr.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
Assertion psrmulr 
|- .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrmulr.s 
 |-  S = ( I mPwSer R )
2 psrmulr.b 
 |-  B = ( Base ` S )
3 psrmulr.m 
 |-  .x. = ( .r ` R )
4 psrmulr.t 
 |-  .xb = ( .r ` S )
5 psrmulr.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( +g ` R ) = ( +g ` R )
8 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
9 simpl 
 |-  ( ( I e. _V /\ R e. _V ) -> I e. _V )
10 1 6 5 2 9 psrbas 
 |-  ( ( I e. _V /\ R e. _V ) -> B = ( ( Base ` R ) ^m D ) )
11 eqid 
 |-  ( +g ` S ) = ( +g ` S )
12 1 2 7 11 psrplusg 
 |-  ( +g ` S ) = ( oF ( +g ` R ) |` ( B X. B ) )
13 eqid 
 |-  ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
14 eqid 
 |-  ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
15 eqidd 
 |-  ( ( I e. _V /\ R e. _V ) -> ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) )
16 simpr 
 |-  ( ( I e. _V /\ R e. _V ) -> R e. _V )
17 1 6 7 3 8 5 10 12 13 14 15 9 16 psrval 
 |-  ( ( I e. _V /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
18 17 fveq2d 
 |-  ( ( I e. _V /\ R e. _V ) -> ( .r ` S ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
19 2 fvexi 
 |-  B e. _V
20 19 19 mpoex 
 |-  ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) e. _V
21 psrvalstr 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >.
22 mulrid 
 |-  .r = Slot ( .r ` ndx )
23 snsstp3 
 |-  { <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. }
24 ssun1 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
25 23 24 sstri 
 |-  { <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
26 21 22 25 strfv 
 |-  ( ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) e. _V -> ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
27 20 26 ax-mp 
 |-  ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) = ( .r ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
28 18 4 27 3eqtr4g 
 |-  ( ( I e. _V /\ R e. _V ) -> .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) )
29 22 str0 
 |-  (/) = ( .r ` (/) )
30 29 eqcomi 
 |-  ( .r ` (/) ) = (/)
31 reldmpsr 
 |-  Rel dom mPwSer
32 31 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
33 1 32 syl5eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> S = (/) )
34 33 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( .r ` S ) = ( .r ` (/) ) )
35 4 34 syl5eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb = ( .r ` (/) ) )
36 33 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( Base ` S ) = ( Base ` (/) ) )
37 base0 
 |-  (/) = ( Base ` (/) )
38 36 2 37 3eqtr4g 
 |-  ( -. ( I e. _V /\ R e. _V ) -> B = (/) )
39 38 olcd 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( B = (/) \/ B = (/) ) )
40 0mpo0 
 |-  ( ( B = (/) \/ B = (/) ) -> ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) = (/) )
41 39 40 syl 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) = (/) )
42 30 35 41 3eqtr4a 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) )
43 28 42 pm2.61i 
 |-  .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )