Metamath Proof Explorer

Theorem psrbas

Description: The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 8-Jul-2019)

Ref Expression
Hypotheses psrbas.s 
|- S = ( I mPwSer R )
psrbas.k 
|- K = ( Base ` R )
psrbas.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbas.b 
|- B = ( Base ` S )
psrbas.i 
|- ( ph -> I e. V )
Assertion psrbas 
|- ( ph -> B = ( K ^m D ) )

Proof

Step Hyp Ref Expression
1 psrbas.s 
 |-  S = ( I mPwSer R )
2 psrbas.k 
 |-  K = ( Base ` R )
3 psrbas.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
4 psrbas.b 
 |-  B = ( Base ` S )
5 psrbas.i 
 |-  ( ph -> I e. V )
6 eqid 
 |-  ( +g ` R ) = ( +g ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
9 eqidd 
 |-  ( ( ph /\ R e. _V ) -> ( K ^m D ) = ( K ^m D ) )
10 eqid 
 |-  ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) = ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) )
11 eqid 
 |-  ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) = ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) )
12 eqid 
 |-  ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) = ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) )
13 eqidd 
 |-  ( ( ph /\ R e. _V ) -> ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) )
14 5 adantr 
 |-  ( ( ph /\ R e. _V ) -> I e. V )
15 simpr 
 |-  ( ( ph /\ R e. _V ) -> R e. _V )
16 1 2 6 7 8 3 9 10 11 12 13 14 15 psrval 
 |-  ( ( ph /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
17 16 fveq2d 
 |-  ( ( ph /\ R e. _V ) -> ( Base ` S ) = ( Base ` ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
18 ovex 
 |-  ( K ^m D ) e. _V
19 psrvalstr 
 |-  ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >.
20 baseid 
 |-  Base = Slot ( Base ` ndx )
21 snsstp1 
 |-  { <. ( Base ` ndx ) , ( K ^m D ) >. } C_ { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. }
22 ssun1 
 |-  { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
23 21 22 sstri 
 |-  { <. ( Base ` ndx ) , ( K ^m D ) >. } C_ ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } )
24 19 20 23 strfv 
 |-  ( ( K ^m D ) e. _V -> ( K ^m D ) = ( Base ` ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) )
25 18 24 ax-mp 
 |-  ( K ^m D ) = ( Base ` ( { <. ( Base ` ndx ) , ( K ^m D ) >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( ( K ^m D ) X. ( K ^m D ) ) ) >. , <. ( .r ` ndx ) , ( g e. ( K ^m D ) , h e. ( K ^m D ) |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( g ` x ) ( .r ` R ) ( h ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , g e. ( K ^m D ) |-> ( ( D X. { x } ) oF ( .r ` R ) g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) )
26 17 4 25 3eqtr4g 
 |-  ( ( ph /\ R e. _V ) -> B = ( K ^m D ) )
27 reldmpsr 
 |-  Rel dom mPwSer
28 27 ovprc2 
 |-  ( -. R e. _V -> ( I mPwSer R ) = (/) )
29 28 adantl 
 |-  ( ( ph /\ -. R e. _V ) -> ( I mPwSer R ) = (/) )
30 1 29 syl5eq 
 |-  ( ( ph /\ -. R e. _V ) -> S = (/) )
31 30 fveq2d 
 |-  ( ( ph /\ -. R e. _V ) -> ( Base ` S ) = ( Base ` (/) ) )
32 base0 
 |-  (/) = ( Base ` (/) )
33 31 4 32 3eqtr4g 
 |-  ( ( ph /\ -. R e. _V ) -> B = (/) )
34 fvprc 
 |-  ( -. R e. _V -> ( Base ` R ) = (/) )
35 34 adantl 
 |-  ( ( ph /\ -. R e. _V ) -> ( Base ` R ) = (/) )
36 2 35 syl5eq 
 |-  ( ( ph /\ -. R e. _V ) -> K = (/) )
37 3 fczpsrbag 
 |-  ( I e. V -> ( x e. I |-> 0 ) e. D )
38 5 37 syl 
 |-  ( ph -> ( x e. I |-> 0 ) e. D )
39 38 adantr 
 |-  ( ( ph /\ -. R e. _V ) -> ( x e. I |-> 0 ) e. D )
40 39 ne0d 
 |-  ( ( ph /\ -. R e. _V ) -> D =/= (/) )
41 2 fvexi 
 |-  K e. _V
42 ovex 
 |-  ( NN0 ^m I ) e. _V
43 3 42 rabex2 
 |-  D e. _V
44 41 43 map0 
 |-  ( ( K ^m D ) = (/) <-> ( K = (/) /\ D =/= (/) ) )
45 36 40 44 sylanbrc 
 |-  ( ( ph /\ -. R e. _V ) -> ( K ^m D ) = (/) )
46 33 45 eqtr4d 
 |-  ( ( ph /\ -. R e. _V ) -> B = ( K ^m D ) )
47 26 46 pm2.61dan 
 |-  ( ph -> B = ( K ^m D ) )