Metamath Proof Explorer

Theorem psrvscafval

Description: The scalar 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-Nov-2024)

Ref Expression
Hypotheses psrvsca.s 
|- S = ( I mPwSer R )
psrvsca.n 
|- .xb = ( .s ` S )
psrvsca.k 
|- K = ( Base ` R )
psrvsca.b 
|- B = ( Base ` S )
psrvsca.m 
|- .x. = ( .r ` R )
psrvsca.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
Assertion psrvscafval 
|- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )

Proof

Step Hyp Ref Expression
1 psrvsca.s 
 |-  S = ( I mPwSer R )
2 psrvsca.n 
 |-  .xb = ( .s ` S )
3 psrvsca.k 
 |-  K = ( Base ` R )
4 psrvsca.b 
 |-  B = ( Base ` S )
5 psrvsca.m 
 |-  .x. = ( .r ` R )
6 psrvsca.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
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 3 6 4 9 psrbas 
 |-  ( ( I e. _V /\ R e. _V ) -> B = ( K ^m D ) )
11 eqid 
 |-  ( +g ` S ) = ( +g ` S )
12 1 4 7 11 psrplusg 
 |-  ( +g ` S ) = ( oF ( +g ` R ) |` ( B X. B ) )
13 eqid 
 |-  ( .r ` S ) = ( .r ` S )
14 1 4 5 13 6 psrmulr 
 |-  ( .r ` S ) = ( 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 ) ) ) ) ) ) )
15 eqid 
 |-  ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
16 eqidd 
 |-  ( ( I e. _V /\ R e. _V ) -> ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) )
17 simpr 
 |-  ( ( I e. _V /\ R e. _V ) -> R e. _V )
18 1 3 7 5 8 6 10 12 14 15 16 9 17 psrval 
 |-  ( ( I e. _V /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
19 18 fveq2d 
 |-  ( ( I e. _V /\ R e. _V ) -> ( .s ` S ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
20 3 fvexi 
 |-  K e. _V
21 4 fvexi 
 |-  B e. _V
22 20 21 mpoex 
 |-  ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) e. _V
23 psrvalstr 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >.
24 vscaid 
 |-  .s = Slot ( .s ` ndx )
25 snsstp2 
 |-  { <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. } C_ { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. }
26 ssun2 
 |-  { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
27 25 26 sstri 
 |-  { <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
28 23 24 27 strfv 
 |-  ( ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) e. _V -> ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
29 22 28 ax-mp 
 |-  ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
30 19 2 29 3eqtr4g 
 |-  ( ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) )
31 eqid 
 |-  (/) = (/)
32 fn0 
 |-  ( (/) Fn (/) <-> (/) = (/) )
33 31 32 mpbir 
 |-  (/) Fn (/)
34 reldmpsr 
 |-  Rel dom mPwSer
35 34 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
36 1 35 eqtrid 
 |-  ( -. ( I e. _V /\ R e. _V ) -> S = (/) )
37 36 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( .s ` S ) = ( .s ` (/) ) )
38 24 str0 
 |-  (/) = ( .s ` (/) )
39 37 2 38 3eqtr4g 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb = (/) )
40 34 1 4 elbasov 
 |-  ( f e. B -> ( I e. _V /\ R e. _V ) )
41 40 con3i 
 |-  ( -. ( I e. _V /\ R e. _V ) -> -. f e. B )
42 41 eq0rdv 
 |-  ( -. ( I e. _V /\ R e. _V ) -> B = (/) )
43 42 xpeq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( K X. B ) = ( K X. (/) ) )
44 xp0 
 |-  ( K X. (/) ) = (/)
45 43 44 eqtrdi 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( K X. B ) = (/) )
46 39 45 fneq12d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( .xb Fn ( K X. B ) <-> (/) Fn (/) ) )
47 33 46 mpbiri 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb Fn ( K X. B ) )
48 fnov 
 |-  ( .xb Fn ( K X. B ) <-> .xb = ( x e. K , f e. B |-> ( x .xb f ) ) )
49 47 48 sylib 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( x .xb f ) ) )
50 41 pm2.21d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( f e. B -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) ) )
51 50 a1d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( x e. K -> ( f e. B -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) ) ) )
52 51 3imp 
 |-  ( ( -. ( I e. _V /\ R e. _V ) /\ x e. K /\ f e. B ) -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) )
53 52 mpoeq3dva 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( x e. K , f e. B |-> ( x .xb f ) ) )
54 49 53 eqtr4d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) )
55 30 54 pm2.61i 
 |-  .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )