Metamath Proof Explorer

Theorem esumsnf

Description: The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017) (Revised by Thierry Arnoux, 2-May-2020)

Ref Expression
Hypotheses esumsnf.0 
|- F/_ k B
esumsnf.1 
|- ( ( ph /\ k = M ) -> A = B )
esumsnf.2 
|- ( ph -> M e. V )
esumsnf.3 
|- ( ph -> B e. ( 0 [,] +oo ) )
Assertion esumsnf 
|- ( ph -> sum* k e. { M } A = B )

Proof

Step Hyp Ref Expression
1 esumsnf.0 
 |-  F/_ k B
2 esumsnf.1 
 |-  ( ( ph /\ k = M ) -> A = B )
3 esumsnf.2 
 |-  ( ph -> M e. V )
4 esumsnf.3 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
5 df-esum 
 |-  sum* k e. { M } A = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. { M } |-> A ) )
6 5 a1i 
 |-  ( ph -> sum* k e. { M } A = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. { M } |-> A ) ) )
7 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
8 snfi 
 |-  { M } e. Fin
9 8 a1i 
 |-  ( ph -> { M } e. Fin )
10 elsni 
 |-  ( k e. { M } -> k = M )
11 10 2 sylan2 
 |-  ( ( ph /\ k e. { M } ) -> A = B )
12 11 mpteq2dva 
 |-  ( ph -> ( k e. { M } |-> A ) = ( k e. { M } |-> B ) )
13 fmptsn 
 |-  ( ( M e. V /\ B e. ( 0 [,] +oo ) ) -> { <. M , B >. } = ( l e. { M } |-> B ) )
14 nfcv 
 |-  F/_ l B
15 eqidd 
 |-  ( k = l -> B = B )
16 14 1 15 cbvmpt 
 |-  ( k e. { M } |-> B ) = ( l e. { M } |-> B )
17 13 16 eqtr4di 
 |-  ( ( M e. V /\ B e. ( 0 [,] +oo ) ) -> { <. M , B >. } = ( k e. { M } |-> B ) )
18 3 4 17 syl2anc 
 |-  ( ph -> { <. M , B >. } = ( k e. { M } |-> B ) )
19 12 18 eqtr4d 
 |-  ( ph -> ( k e. { M } |-> A ) = { <. M , B >. } )
20 fsng 
 |-  ( ( M e. V /\ B e. ( 0 [,] +oo ) ) -> ( ( k e. { M } |-> A ) : { M } --> { B } <-> ( k e. { M } |-> A ) = { <. M , B >. } ) )
21 3 4 20 syl2anc 
 |-  ( ph -> ( ( k e. { M } |-> A ) : { M } --> { B } <-> ( k e. { M } |-> A ) = { <. M , B >. } ) )
22 19 21 mpbird 
 |-  ( ph -> ( k e. { M } |-> A ) : { M } --> { B } )
23 4 snssd 
 |-  ( ph -> { B } C_ ( 0 [,] +oo ) )
24 22 23 fssd 
 |-  ( ph -> ( k e. { M } |-> A ) : { M } --> ( 0 [,] +oo ) )
25 xrltso 
 |-  < Or RR*
26 25 a1i 
 |-  ( ph -> < Or RR* )
27 0xr 
 |-  0 e. RR*
28 27 a1i 
 |-  ( ph -> 0 e. RR* )
29 elxrge0 
 |-  ( B e. ( 0 [,] +oo ) <-> ( B e. RR* /\ 0 <_ B ) )
30 4 29 sylib 
 |-  ( ph -> ( B e. RR* /\ 0 <_ B ) )
31 30 simpld 
 |-  ( ph -> B e. RR* )
32 suppr 
 |-  ( ( < Or RR* /\ 0 e. RR* /\ B e. RR* ) -> sup ( { 0 , B } , RR* , < ) = if ( B < 0 , 0 , B ) )
33 26 28 31 32 syl3anc 
 |-  ( ph -> sup ( { 0 , B } , RR* , < ) = if ( B < 0 , 0 , B ) )
34 0fin 
 |-  (/) e. Fin
35 34 a1i 
 |-  ( ph -> (/) e. Fin )
36 reseq2 
 |-  ( x = (/) -> ( ( k e. { M } |-> A ) |` x ) = ( ( k e. { M } |-> A ) |` (/) ) )
37 res0 
 |-  ( ( k e. { M } |-> A ) |` (/) ) = (/)
38 36 37 eqtrdi 
 |-  ( x = (/) -> ( ( k e. { M } |-> A ) |` x ) = (/) )
39 38 oveq2d 
 |-  ( x = (/) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum (/) ) )
40 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
41 40 gsum0 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum (/) ) = 0
42 39 41 eqtrdi 
 |-  ( x = (/) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = 0 )
43 42 adantl 
 |-  ( ( ph /\ x = (/) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = 0 )
44 reseq2 
 |-  ( x = { M } -> ( ( k e. { M } |-> A ) |` x ) = ( ( k e. { M } |-> A ) |` { M } ) )
45 ssid 
 |-  { M } C_ { M }
46 resmpt 
 |-  ( { M } C_ { M } -> ( ( k e. { M } |-> A ) |` { M } ) = ( k e. { M } |-> A ) )
47 45 46 ax-mp 
 |-  ( ( k e. { M } |-> A ) |` { M } ) = ( k e. { M } |-> A )
48 44 47 eqtrdi 
 |-  ( x = { M } -> ( ( k e. { M } |-> A ) |` x ) = ( k e. { M } |-> A ) )
49 48 oveq2d 
 |-  ( x = { M } -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. { M } |-> A ) ) )
50 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
51 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
52 cmnmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
53 51 52 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
54 53 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
55 nfv 
 |-  F/ k ph
56 50 54 3 4 2 55 1 gsumsnfd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. { M } |-> A ) ) = B )
57 49 56 sylan9eqr 
 |-  ( ( ph /\ x = { M } ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = B )
58 35 9 28 4 43 57 fmptpr 
 |-  ( ph -> { <. (/) , 0 >. , <. { M } , B >. } = ( x e. { (/) , { M } } |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) )
59 pwsn 
 |-  ~P { M } = { (/) , { M } }
60 prssi 
 |-  ( ( (/) e. Fin /\ { M } e. Fin ) -> { (/) , { M } } C_ Fin )
61 34 8 60 mp2an 
 |-  { (/) , { M } } C_ Fin
62 59 61 eqsstri 
 |-  ~P { M } C_ Fin
63 df-ss 
 |-  ( ~P { M } C_ Fin <-> ( ~P { M } i^i Fin ) = ~P { M } )
64 62 63 mpbi 
 |-  ( ~P { M } i^i Fin ) = ~P { M }
65 64 59 eqtri 
 |-  ( ~P { M } i^i Fin ) = { (/) , { M } }
66 eqid 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) )
67 65 66 mpteq12i 
 |-  ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) = ( x e. { (/) , { M } } |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) )
68 58 67 eqtr4di 
 |-  ( ph -> { <. (/) , 0 >. , <. { M } , B >. } = ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) )
69 68 rneqd 
 |-  ( ph -> ran { <. (/) , 0 >. , <. { M } , B >. } = ran ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) )
70 rnpropg 
 |-  ( ( (/) e. Fin /\ { M } e. Fin ) -> ran { <. (/) , 0 >. , <. { M } , B >. } = { 0 , B } )
71 35 9 70 syl2anc 
 |-  ( ph -> ran { <. (/) , 0 >. , <. { M } , B >. } = { 0 , B } )
72 69 71 eqtr3d 
 |-  ( ph -> ran ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) = { 0 , B } )
73 72 supeq1d 
 |-  ( ph -> sup ( ran ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) , RR* , < ) = sup ( { 0 , B } , RR* , < ) )
74 30 simprd 
 |-  ( ph -> 0 <_ B )
75 xrlenlt 
 |-  ( ( 0 e. RR* /\ B e. RR* ) -> ( 0 <_ B <-> -. B < 0 ) )
76 28 31 75 syl2anc 
 |-  ( ph -> ( 0 <_ B <-> -. B < 0 ) )
77 74 76 mpbid 
 |-  ( ph -> -. B < 0 )
78 eqidd 
 |-  ( ph -> B = B )
79 77 78 jca 
 |-  ( ph -> ( -. B < 0 /\ B = B ) )
80 79 olcd 
 |-  ( ph -> ( ( B < 0 /\ B = 0 ) \/ ( -. B < 0 /\ B = B ) ) )
81 eqif 
 |-  ( B = if ( B < 0 , 0 , B ) <-> ( ( B < 0 /\ B = 0 ) \/ ( -. B < 0 /\ B = B ) ) )
82 80 81 sylibr 
 |-  ( ph -> B = if ( B < 0 , 0 , B ) )
83 33 73 82 3eqtr4rd 
 |-  ( ph -> B = sup ( ran ( x e. ( ~P { M } i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( ( k e. { M } |-> A ) |` x ) ) ) , RR* , < ) )
84 7 9 24 83 xrge0tsmsd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. { M } |-> A ) ) = { B } )
85 84 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. { M } |-> A ) ) = U. { B } )
86 unisng 
 |-  ( B e. ( 0 [,] +oo ) -> U. { B } = B )
87 4 86 syl 
 |-  ( ph -> U. { B } = B )
88 6 85 87 3eqtrd 
 |-  ( ph -> sum* k e. { M } A = B )