Metamath Proof Explorer

Theorem psrsca

Description: The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrsca.s 
|- S = ( I mPwSer R )
psrsca.i 
|- ( ph -> I e. V )
psrsca.r 
|- ( ph -> R e. W )
Assertion psrsca 
|- ( ph -> R = ( Scalar ` S ) )

Proof

Step Hyp Ref Expression
1 psrsca.s 
 |-  S = ( I mPwSer R )
2 psrsca.i 
 |-  ( ph -> I e. V )
3 psrsca.r 
 |-  ( ph -> R e. W )
4 psrvalstr 
 |-  ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >.
5 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
6 snsstp1 
 |-  { <. ( Scalar ` ndx ) , R >. } C_ { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. }
7 ssun2 
 |-  { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } C_ ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } )
8 6 7 sstri 
 |-  { <. ( Scalar ` ndx ) , R >. } C_ ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } )
9 4 5 8 strfv 
 |-  ( R e. W -> R = ( Scalar ` ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) )
10 3 9 syl 
 |-  ( ph -> R = ( Scalar ` ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( +g ` R ) = ( +g ` R )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
15 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
16 eqid 
 |-  ( Base ` S ) = ( Base ` S )
17 1 11 15 16 2 psrbas 
 |-  ( ph -> ( Base ` S ) = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
18 eqid 
 |-  ( +g ` S ) = ( +g ` S )
19 1 16 12 18 psrplusg 
 |-  ( +g ` S ) = ( oF ( +g ` R ) |` ( ( Base ` S ) X. ( Base ` S ) ) )
20 eqid 
 |-  ( .r ` S ) = ( .r ` S )
21 1 16 13 20 15 psrmulr 
 |-  ( .r ` S ) = ( f e. ( Base ` S ) , z e. ( Base ` S ) |-> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ w } |-> ( ( f ` x ) ( .r ` R ) ( z ` ( w oF - x ) ) ) ) ) ) )
22 eqid 
 |-  ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) = ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) )
23 eqidd 
 |-  ( ph -> ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) )
24 1 11 12 13 14 15 17 19 21 22 23 2 3 psrval 
 |-  ( ph -> S = ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) )
25 24 fveq2d 
 |-  ( ph -> ( Scalar ` S ) = ( Scalar ` ( { <. ( Base ` ndx ) , ( Base ` S ) >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. ( Base ` S ) |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) )
26 10 25 eqtr4d 
 |-  ( ph -> R = ( Scalar ` S ) )