Metamath Proof Explorer

Theorem psrplusg

Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psrplusg.s 
|- S = ( I mPwSer R )
psrplusg.b 
|- B = ( Base ` S )
psrplusg.a 
|- .+ = ( +g ` R )
psrplusg.p 
|- .+b = ( +g ` S )
Assertion psrplusg 
|- .+b = ( oF .+ |` ( B X. B ) )

Proof

Step Hyp Ref Expression
1 psrplusg.s 
 |-  S = ( I mPwSer R )
2 psrplusg.b 
 |-  B = ( Base ` S )
3 psrplusg.a 
 |-  .+ = ( +g ` R )
4 psrplusg.p 
 |-  .+b = ( +g ` S )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
8 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
9 simpl 
 |-  ( ( I e. _V /\ R e. _V ) -> I e. _V )
10 1 5 8 2 9 psrbas 
 |-  ( ( I e. _V /\ R e. _V ) -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
11 eqid 
 |-  ( oF .+ |` ( B X. B ) ) = ( oF .+ |` ( B X. B ) )
12 eqid 
 |-  ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) = ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) )
13 eqid 
 |-  ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) = ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) )
14 eqidd 
 |-  ( ( I e. _V /\ R e. _V ) -> ( 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 ) } ) ) )
15 simpr 
 |-  ( ( I e. _V /\ R e. _V ) -> R e. _V )
16 1 5 3 6 7 8 10 11 12 13 14 9 15 psrval 
 |-  ( ( I e. _V /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 ) } ) ) >. } ) )
17 16 fveq2d 
 |-  ( ( I e. _V /\ R e. _V ) -> ( +g ` S ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 ) } ) ) >. } ) ) )
18 2 fvexi 
 |-  B e. _V
19 18 18 xpex 
 |-  ( B X. B ) e. _V
20 ofexg 
 |-  ( ( B X. B ) e. _V -> ( oF .+ |` ( B X. B ) ) e. _V )
21 psrvalstr 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 >.
22 plusgid 
 |-  +g = Slot ( +g ` ndx )
23 snsstp2 
 |-  { <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. }
24 ssun1 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 23 24 sstri 
 |-  { <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 21 22 25 strfv 
 |-  ( ( oF .+ |` ( B X. B ) ) e. _V -> ( oF .+ |` ( B X. B ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 ) } ) ) >. } ) ) )
27 19 20 26 mp2b 
 |-  ( oF .+ |` ( B X. B ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k 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 <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { 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 ) } ) ) >. } ) )
28 17 4 27 3eqtr4g 
 |-  ( ( I e. _V /\ R e. _V ) -> .+b = ( oF .+ |` ( B X. B ) ) )
29 reldmpsr 
 |-  Rel dom mPwSer
30 29 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
31 1 30 syl5eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> S = (/) )
32 31 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( +g ` S ) = ( +g ` (/) ) )
33 22 str0 
 |-  (/) = ( +g ` (/) )
34 32 4 33 3eqtr4g 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .+b = (/) )
35 31 fveq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( Base ` S ) = ( Base ` (/) ) )
36 base0 
 |-  (/) = ( Base ` (/) )
37 35 2 36 3eqtr4g 
 |-  ( -. ( I e. _V /\ R e. _V ) -> B = (/) )
38 37 xpeq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( B X. B ) = ( B X. (/) ) )
39 xp0 
 |-  ( B X. (/) ) = (/)
40 38 39 syl6eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( B X. B ) = (/) )
41 40 reseq2d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( oF .+ |` ( B X. B ) ) = ( oF .+ |` (/) ) )
42 res0 
 |-  ( oF .+ |` (/) ) = (/)
43 41 42 syl6eq 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( oF .+ |` ( B X. B ) ) = (/) )
44 34 43 eqtr4d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> .+b = ( oF .+ |` ( B X. B ) ) )
45 28 44 pm2.61i 
 |-  .+b = ( oF .+ |` ( B X. B ) )